High-contrast homogenization: Provider.PolynomialHomogenization.RootAssembly

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The homogenization root from the quenched scale and the deterministic package

The root theorem splits in two. The random side produces the homogenized block, the polynomial length, the measurable scale with its two-part tail, and one integer-translation-invariant full-measure event on which the weighted block row decays past that scale. The deterministic side turns the block-row certificate at a sample into the homogenized matrix, one corrector family, and the five estimates.

This module composes the two sides. It proves no estimate: every deterministic input is carried as one hypothesis, and the two abstract predicates below name the interfaces along which the deterministic modules communicate. The first is the normalized weak-error certificate that the block row is converted into; the second is the characterization of the corrector family that its estimates are read against.

The reconciliation of the shared constant and the shared error exponent is performed here, since every clause is weakened by enlarging the constant and by shrinking the exponent.

Why the certificate interface is threaded, folded and law-free

Three conventions fix the shape of the interface below; Lean checks none of them, so they are recorded here.

• The certificate is per g and per rate. GoodScale takes two leading real arguments, the stochastic exponent g and the certificate's own decay rate κ, and every deterministic input reads GoodScale g κ abar a x under its own ∀ g ∈ Ico 0 1, ∀ κ, 0 < κ; an input that does not use them may ignore them. The rate is threaded rather than existentially hidden because the Dirichlet estimate's exponent is the certificate's rate, so it cannot be chosen before the certificate is seen. The Dirichlet input therefore takes the rate as a parameter together with the order constraint κ ≤ (1 + g) / 4 that the window s₀ ∈ Ico ((1 + g) / 4) (1 / 2) of the root statement forces.

• The provider's constants are law-free but g-dependent, while C₀ sits before g. The Dirichlet input carries a law-free amplitude Lg ≥ 1, chosen together with the eccentricity power after g, which multiplies the scale in both the ε-premise and the rate factor. A g-dependent constant is paid by Lg ^ κ and never by C₀.

• The certificate does not live at the raw quenched scale. The printed-order certificate is produced at the common affine scale, a positive multiple of the quenched scale depending on the homogenized matrix through its witness eccentricity, so hhomogenized exports its own factor Lcert * eccentricityFoldFactor abar pCert and concludes at the enlarged scale. Both factors are law-free times an eccentricity power, so their product is again polynomial in the printed length base.

The exported length is X a * rootLengthFactor abar Lcert pCert Lg pEcc and the polynomial exponent is enlarged by rootLengthExponent Lcert pCert Lg pEcc.

theorem HCPolySupport.HighContrast.RootInterface.polynomial_homogenization_of_quenched_scale (d : ℕ) (hd : 2 ≤ d) (GoodScale : ℝ → ℝ → Mat d → CoeffSpace d → ℝ → Prop) (CorrectorFamily : Mat d → (Vec d → CoeffSpace d → Vec d → ℝ) → (Vec d → CoeffSpace d → Vec d → Vec d) → Prop) (hquenched : ∃ (cd : ℝ), 0 < cd ∧ ∀ g ∈ Set.Ico 0 1, ∃ (C : ℝ) (cSrc : ℝ) (kappa : ℝ) (delta : ℝ), 0 < C ∧ 0 < cSrc ∧ 0 < kappa ∧ delta ∈ Set.Ioo 0 1 ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Psi K S → ∃ (Abar : BlockMat d) (Nann : ℕ) (alpha : ℝ) (Lpoly : ℝ) (Ssrc : CoeffSpace d → ℝ) (X : CoeffSpace d → ℝ), 0 < alpha ∧ IsSymmetricBlockMat Abar ∧ Book.Ch02.BlockPosDef Abar ∧ (∀ (m : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑m))) ∧ (∀ (m : ℕ), BlockMatLoewnerLE (blockSharp (annealedBlock P (centeredCube d ↑m))) Abar) ∧ (∀ (j : ℕ), annealedContrast P ↑(Nann + j) - 1 ≤ 3 ^ (-alpha * ↑j)) ∧ (∀ (a : CoeffSpace d), Ssrc a = max 1 (S a / 3 ^ Nann)) ∧ 1 ≤ Lpoly ∧ Lpoly ≤ (2 + aspectRatio E * K) ^ C ∧ Measurable Ssrc ∧ (∀ (a : CoeffSpace d), 1 ≤ Ssrc a) ∧ Measurable X ∧ (∀ (a : CoeffSpace d), 1 ≤ X a) ∧ (∀ (a : CoeffSpace d), S a ≤ X a) ∧ (∀ (t : ℝ), 1 ≤ t → P.real {a : CoeffSpace d | C * Lpoly * t ≤ X a} ≤ Real.exp (-cd * t ^ (↑d - 2 * g)) + (Psi (cSrc * t))⁻¹) ∧ ∃ (OmegaEnd : Set (CoeffSpace d)), MeasurableSet OmegaEnd ∧ P.real OmegaEnd = 1 ∧ (∀ (z : Fin d → ℤ), translateCoeff z ⁻¹' OmegaEnd = OmegaEnd) ∧ ∀ a ∈ OmegaEnd, Quenched.HasAllLaterPhysicalBlockRow ((1 + 3 * g) / 4) kappa delta Abar S X a) (hhomogenized : ∀ g ∈ Set.Ico 0 1, ∀ (kappa delta : ℝ), 0 < kappa → delta ∈ Set.Ioo 0 1 → ∃ (kappaRate : ℝ) (Lcert : ℝ) (pCert : ℝ), 0 < kappaRate ∧ kappaRate ≤ (1 + g) / 4 ∧ 1 ≤ Lcert ∧ 0 ≤ pCert ∧ ∀ (abar : Mat d), Matrix.PosDef (symmPart abar) → ∀ (Omega : Set (CoeffSpace d)) (S X : CoeffSpace d → ℝ), (∀ (z : Fin d → ℤ), translateCoeff z ⁻¹' Omega = Omega) → (∀ b ∈ Omega, 1 ≤ X b) → (∀ b ∈ Omega, S b ≤ X b) → (∀ b ∈ Omega, Quenched.HasAllLaterPhysicalBlockRow ((1 + 3 * g) / 4) kappa delta (Book.Ch02.constantBlockMatrix abar) S X b) → ∀ a ∈ Omega, GoodScale g kappaRate abar a (X a * (Lcert * RowSupply.eccentricityFoldFactor abar pCert))) (hdirichlet : ∃ (C₀ : ℝ → ℝ → ℝ → ℝ), (∀ (s₀ ρ Rad : ℝ), 0 < C₀ s₀ ρ Rad) ∧ ∀ g ∈ Set.Ico 0 1, ∀ (κ : ℝ), 0 < κ → κ ≤ (1 + g) / 4 → ∃ (Lg : ℝ) (pEcc : ℝ), 1 ≤ Lg ∧ 0 ≤ pEcc ∧ ∀ (abar : Mat d) (a : CoeffSpace d) (x : ℝ), 1 ≤ x → GoodScale g κ abar a x → ∀ s₀ ∈ Set.Ico ((1 + g) / 4) (1 / 2), ∀ (ρ Rad : ℝ) (U : Set (Vec d)), (∃ (j : ℤ) (z : Vec d), U = (fun (y : Vec d) => z + matVecMul (matSqrt (symmPart abar)) y) '' openCubeSet (originCube d j)) → HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) ρ Rad → U ⊆ ellipsoid abar 1 → ellipsoid abar (1 / (3 * √↑d)) ⊆ U → ∀ (ε : ℝ), 0 < ε → x * (Lg * RowSupply.eccentricityFoldFactor abar pEcc) ≤ ε⁻¹ → ∀ (g₀ : H1Function U), (∃ (Lb : ℝ), ∀ᵐ (y : Vec d) ∂MeasureTheory.volume.restrict U, |g₀.toFun y| + √(vecNormSq (g₀.grad y)) ≤ Lb) → hsNormSq U s₀ g₀.grad ≠ ⊤ → ∀ (h : H1Function U), MemAffineH10 U g₀ h → IsWeakSolutionOn (fun (x : Vec d) => abar) U h.grad → ∀ (uFun : Vec d → ℝ) (uGrad : Vec d → Vec d), (MemH1a0 (scaledCoeff ε a) U (fun (y : Vec d) => uFun y - g₀.toFun y) fun (y : Vec d) => uGrad y - g₀.grad y) → IsWeakSolutionOn (scaledCoeff ε a) U uGrad → ((negSobolevNorm U s₀ fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (uGrad y - h.grad y)) + negSobolevNorm U s₀ fun (y : Vec d) => matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (scaledCoeff ε a y - skewPart abar) (uGrad y) - matVecMul (symmPart abar) (h.grad y))) ≤ ENNReal.ofReal (C₀ s₀ ρ Rad * (ε * (x * (Lg * RowSupply.eccentricityFoldFactor abar pEcc))) ^ κ) * (hsNormSq U s₀ fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (g₀.grad y)) ^ (1 / 2)) (hcorrector : ∀ g ∈ Set.Ico 0 1, ∀ (κ : ℝ), 0 < κ → ∀ (abar : Mat d), Matrix.PosDef (symmPart abar) → ∃ (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), CorrectorFamily abar Phi gradPhi ∧ (∀ (c : ℝ) (e e' : Vec d) (a : CoeffSpace d), gradPhi (c • e + e') a =ᵐ[MeasureTheory.volume] fun (x : Vec d) => c • gradPhi e a x + gradPhi e' a x) ∧ (∀ (z : Fin d → ℤ) (e : Vec d) (a : CoeffSpace d), gradPhi e (translateCoeff z a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => gradPhi e a (x + Source.AKL.intTranslation z)) ∧ ∀ (a : CoeffSpace d) (x : ℝ), GoodScale g κ abar a x → ∀ (e : Vec d), HasWeakGradientOn Set.univ (Phi e a) (gradPhi e a) ∧ IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) Set.univ fun (y : Vec d) => e + gradPhi e a y) (hcorrectorDecay : ∀ g ∈ Set.Ico 0 1, ∀ (κc : ℝ), 0 < κc → ∃ (C : ℝ) (κ : ℝ), 0 < C ∧ 0 < κ ∧ ∀ (abar : Mat d) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), CorrectorFamily abar Phi gradPhi → ∀ (a : CoeffSpace d) (x : ℝ), 1 ≤ x → GoodScale g κc abar a x → ∀ (e : Vec d) (r : ℝ), x ≤ r → ((ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (gradPhi e a y)) + ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) fun (y : Vec d) => matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (↑↑a y - skewPart abar) (e + gradPhi e a y) - matVecMul (symmPart abar) e)) ≤ ENNReal.ofReal (C * √(vecDot e (matVecMul (symmPart abar) e)) * (r / x) ^ (-κ))) (hliouville : ∀ g ∈ Set.Ico 0 1, ∀ (κc : ℝ), 0 < κc → ∀ (abar : Mat d) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), CorrectorFamily abar Phi gradPhi → ∀ (a : CoeffSpace d) (x : ℝ), GoodScale g κc abar a x → ∀ ϑ ∈ Set.Ioo 0 1, (∀ (v : Vec d → ℝ) (Dv : Vec d → Vec d), MemLiouvilleClass (fun (y : Vec d) => ↑↑a y) ϑ v Dv → ∃ (e : Vec d) (c : ℝ), v =ᵐ[MeasureTheory.volume] fun (y : Vec d) => vecDot e y + Phi e a y + c) ∧ ∀ (e : Vec d) (c : ℝ), MemLiouvilleClass (fun (y : Vec d) => ↑↑a y) ϑ (fun (y : Vec d) => vecDot e y + Phi e a y + c) fun (y : Vec d) => e + gradPhi e a y) (hlipschitz : ∀ g ∈ Set.Ico 0 1, ∀ (κc : ℝ), 0 < κc → ∃ (C : ℝ), 0 < C ∧ ∀ (abar : Mat d) (a : CoeffSpace d) (x : ℝ), 1 ≤ x → GoodScale g κc abar a x → ∀ (R : ℝ), x ≤ R → ∀ (u : Vec d → ℝ) (Du : Vec d → Vec d), MemH1a (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) u Du → IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du → ∀ r ∈ Set.Icc x R, weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) Du ≤ ENNReal.ofReal C * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du) (hC1 : ∀ g ∈ Set.Ico 0 1, ∀ (κc : ℝ), 0 < κc → ∃ (C₁ : ℝ → ℝ), (∀ (ϑ : ℝ), 0 < C₁ ϑ) ∧ ∀ (abar : Mat d) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), CorrectorFamily abar Phi gradPhi → ∀ (a : CoeffSpace d) (x : ℝ), 1 ≤ x → GoodScale g κc abar a x → ∀ (R : ℝ), x ≤ R → ∀ (u : Vec d → ℝ) (Du : Vec d → Vec d), MemH1a (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) u Du → IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du → ∀ ϑ ∈ Set.Ioo 0 1, ∃ (e : Vec d), ∀ r ∈ Set.Icc x R, (weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) fun (y : Vec d) => Du y - (e + gradPhi e a y)) ≤ ENNReal.ofReal (C₁ ϑ * (r / R) ^ ϑ) * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du) : ∃ (cd : ℝ) (C₀ : ℝ → ℝ → ℝ → ℝ), 0 < cd ∧ (∀ (s₀ ρ Rad : ℝ), 0 < C₀ s₀ ρ Rad) ∧ ∀ g ∈ Set.Ico 0 1, ∃ (C : ℝ) (cSrc : ℝ) (κ : ℝ) (C₁ : ℝ → ℝ), 0 < C ∧ 0 < cSrc ∧ 0 < κ ∧ (∀ (ϑ : ℝ), 0 < C₁ ϑ) ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Ψ K S → ∃ (abar : Mat d) (Lpoly : ℝ) (X : CoeffSpace d → ℝ) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), 1 ≤ Lpoly ∧ Measurable X ∧ (∀ (a : CoeffSpace d), 1 ≤ X a) ∧ (∀ (c : ℝ) (e e' : Vec d) (a : CoeffSpace d), gradPhi (c • e + e') a =ᵐ[MeasureTheory.volume] fun (x : Vec d) => c • gradPhi e a x + gradPhi e' a x) ∧ (∀ (z : Fin d → ℤ) (e : Vec d) (a : CoeffSpace d), gradPhi e (translateCoeff z a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => gradPhi e a (x + Source.AKL.intTranslation z)) ∧ Lpoly ≤ (2 + aspectRatio E * K) ^ C ∧ (∀ (t : ℝ), 1 ≤ t → P.real {a : CoeffSpace d | C * Lpoly * t ≤ X a} ≤ Real.exp (-cd * t ^ (↑d - 2 * g)) + (Ψ (cSrc * t))⁻¹) ∧ (∀ (x : Vec d), x ≠ 0 → 0 < vecDot x (matVecMul (symmPart abar) x)) ∧ ∃ (Ωend : Set (CoeffSpace d)), MeasurableSet Ωend ∧ P.real Ωend = 1 ∧ (∀ (z : Fin d → ℤ), translateCoeff z ⁻¹' Ωend = Ωend) ∧ (∀ s₀ ∈ Set.Ico ((1 + g) / 4) (1 / 2), ∀ (ρ Rad : ℝ) (U : Set (Vec d)), (∃ (j : ℤ) (z : Vec d), U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) → HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) ρ Rad → U ⊆ ellipsoid abar 1 → ellipsoid abar (1 / (3 * √↑d)) ⊆ U → ∀ a ∈ Ωend, ⋯) ∧ (∀ a ∈ Ωend, ∀ (e : Vec d), HasWeakGradientOn Set.univ (Phi e a) (gradPhi e a) ∧ IsWeakSolutionOn (fun (x : Vec d) => ↑↑a x) Set.univ fun (x : Vec d) => e + gradPhi e a x) ∧ (∀ a ∈ Ωend, ∀ (e : Vec d) (r : ℝ), X a ≤ r → (ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) fun (x : Vec d) => matVecMul (matSqrt (symmPart abar)) (gradPhi e a x)) + ENNReal.ofReal r⁻¹ * ⋯ ≤ ENNReal.ofReal (C * √(vecDot e (matVecMul (symmPart abar) e)) * (r / X a) ^ (-κ))) ∧ (∀ a ∈ Ωend, ∀ ϑ ∈ Set.Ioo 0 1, (∀ (v : Vec d → ℝ) (Dv : Vec d → Vec d), ⋯) ∧ ∀ (e : Vec d) (c : ℝ), ⋯) ∧ ∀ a ∈ Ωend, ∀ (R : ℝ), X a ≤ R → ∀ (u : Vec d → ℝ) (Du : Vec d → Vec d), ⋯ → ⋯

The homogenization root, given the quenched minimal scale and the deterministic package, at the threaded and folded certificate interface.

GoodScale g κ abar a x is the certificate the deterministic modules read: the normalized weak-error condition of stochastic exponent g and decay rate κ satisfied by the sample a above the scale x, relative to the homogenized matrix abar. CorrectorFamily abar Phi gradPhi is the characterization of the corrector family against which the corrector, Liouville and regularity estimates are stated.