High-contrast homogenization: Provider.UniformEllipticity.UniformHomogenization

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

Quantitative homogenization under uniform ellipticity

t.uniform.homogenization is the uniformly elliptic instance of the general polynomial homogenization theorem t.random.homogenization: a ℤ^d-stationary law of unit range whose fields satisfy e.uniform.ellipticity with constants 0 < λ ≤ 1 ≤ Λ carries the whole conclusion list of the general theorem, at discount exponent g = 0, with the homogenization length bounded by a power of 2 + Λ/λ.

The three data the general theorem quantifies over are produced here from e.uniform.ellipticity alone.

• The reference block is the diagonal doubled block diag(2Λ, 2λ⁻¹). On every standard aligned cube the coarse block response of a (λ, Λ)-elliptic field is dominated by it, with no discount factor: the constant competitor is admissible at every cube, and the doubled quadratic form of a (λ, Λ)-elliptic matrix is bounded by 2Λ|p|² + 2λ⁻¹|q|². Its reference aspect ratio is at most 4Λ/λ.
• The gauge is Ψ(t) = exp(t^d), with growth witness 2.
• The source scale is identically zero, so its tail is trivial and the two-part tail of the general theorem collapses: the second term is then exp(-(c t)^d), of the same shape as the first, and a dilation of the scale absorbs both into exp(-t^d), the tail written at e.uniform.scale.tail.

Scope. The Dirichlet clause below is the homogeneous negative-Sobolev estimate of the general theorem, on the adapted cells of the homogenized matrix. The L² estimate e.uniform.dirichlet, which carries a forcing term f and is read on the ellipsoids e.homogenized.ellipsoids, is deduced in the reference text from that estimate by a further duality argument — harmonic replacement on a mesoscopic grid against a constant-coefficient adjoint problem — which is not carried out here. The large-scale energy estimate e.uniform.energy and the first-order approximation are stated on the ellipsoids E_r, as in the reference text.

A representative with the prescribed ellipticity constants

theorem HCPolySupport.HighContrast.exists_pointwise_isEllipticMatrix_representative {d : ℕ} {a : Source.AKL.Field d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (↑a x)) : ∃ (f : CoeffField d), Measurable f ∧ (∀ (x : Vec d), IsEllipticMatrix lam Lam (f x)) ∧ ↑a =ᵐ[MeasureTheory.volume] f

A coefficient field uniformly elliptic almost everywhere with constants (λ, Λ) has a measurable representative uniformly elliptic with the same constants at every point.

The reference block of a uniformly elliptic law

theorem HCPolySupport.HighContrast.blockVecDot_blockMatrixOfCoeff_le_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (p q : Vec d) : blockVecDot (p, q) (blockMatVecMul (blockMatrixOfCoeff A) (p, q)) ≤ 2 * Lam * vecNormSq p + 2 * lam⁻¹ * vecNormSq q

The doubled quadratic form of a (λ, Λ)-elliptic matrix is bounded by 2Λ|p|² + 2λ⁻¹|q|²: the two inequalities of e.uniform.ellipticity read on the Schur blocks as σ + kᵗσ⁻¹k ≤ Λ and σ⁻¹ ≤ λ⁻¹.

noncomputable def HCPolySupport.HighContrast.uniformRefBlock (d : ℕ) (lam Lam : ℝ) : BlockMat d

The reference block of a uniformly elliptic law: the diagonal doubled block diag(2Λ, 2λ⁻¹).

Equations

• HCPolySupport.HighContrast.uniformRefBlock d lam Lam = HCPolySupport.Book.Ch02.blockDiag ((2 * Lam) • 1) ((2 * lam⁻¹) • 1)

theorem HCPolySupport.HighContrast.blockVecDot_uniformRefBlock {d : ℕ} (lam Lam : ℝ) (p q : Vec d) : blockVecDot (p, q) (blockMatVecMul (uniformRefBlock d lam Lam) (p, q)) = 2 * Lam * vecNormSq p + 2 * lam⁻¹ * vecNormSq q

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_uniformRefBlock {d : ℕ} (lam Lam : ℝ) : IsSymmetricBlockMat (uniformRefBlock d lam Lam)

theorem HCPolySupport.HighContrast.blockPosDef_uniformRefBlock {d : ℕ} {lam Lam : ℝ} (hlam : 0 < lam) (hLam : 0 < Lam) : Book.Ch02.BlockPosDef (uniformRefBlock d lam Lam)

Coarse graining preserves uniform ellipticity

theorem HCPolySupport.HighContrast.mu_le_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) {lam Lam : ℝ} {f : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U f) (p q : Vec d) : Mu U (p, q) f ≤ Lam * vecNormSq p + lam⁻¹ * vecNormSq q

The constant competitor bounds the coarse energy of a uniformly elliptic field on every bounded open convex domain of positive volume.

theorem HCPolySupport.HighContrast.volume_standardCell_toReal_pos {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : 0 < (MeasureTheory.volume (standardCell d k w)).toReal

theorem HCPolySupport.HighContrast.coarseBlock_blockMatLoewnerLE_uniformRefBlock {d : ℕ} [NeZero d] {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) {a : CoeffSpace d} (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (↑↑a x)) (k : ℤ) (w : Fin d → ℤ) : BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (uniformRefBlock d lam Lam)

Coarse graining preserves uniform ellipticity. The coarse block response of a field satisfying e.uniform.ellipticity is dominated, on every standard aligned cube and at every scale, by the diagonal reference block diag(2Λ, 2λ⁻¹) — with no discount factor, so the domination holds at the exponent g = 0.

The gauge

noncomputable def HCPolySupport.HighContrast.uniformGauge (d : ℕ) : ℝ → ℝ

The gauge of a uniformly elliptic law: Ψ(t) = exp(t^d).

Equations

• HCPolySupport.HighContrast.uniformGauge d t = Real.exp (t ^ d)

theorem HCPolySupport.HighContrast.admissiblePsi_uniformGauge (d : ℕ) : IndependentSums.AdmissiblePsi (uniformGauge d)

exp(t^d) is an admissible gauge: increasing on ℝ₊ with values in [1, ∞).

theorem HCPolySupport.HighContrast.hasPsiGrowth_uniformGauge {d : ℕ} (hd : 1 ≤ d) : IndependentSums.HasPsiGrowth (uniformGauge d) 2

exp(t^d) has growth witness 2: t exp(t^d) ≤ exp((2t)^d) for t ≥ 1.

The coarse ellipticity bundle

theorem HCPolySupport.HighContrast.coarseEllipticityDagger_of_ae_isEllipticMatrix {d : ℕ} [NeZero d] (hd : 1 ≤ d) {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) {P : MeasureTheory.Measure (CoeffSpace d)} (hell : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (↑↑a x)) : CoarseEllipticityDagger P 0 (uniformRefBlock d lam Lam) (uniformGauge d) 2 fun (x : CoeffSpace d) => 0

A law satisfying e.uniform.ellipticity carries the coarse ellipticity assumption of the general theorem at the exponent g = 0, with the diagonal reference block diag(2Λ, 2λ⁻¹), the gauge exp(t^d), growth witness 2, and the zero source scale.

The reference aspect ratio

theorem HCPolySupport.HighContrast.specBound_smul_one {d : ℕ} [NeZero d] {c : ℝ} (hc : 0 ≤ c) : specBound (c • 1) = c

theorem HCPolySupport.HighContrast.lambdaRef_uniformRefBlock {d : ℕ} [NeZero d] {lam : ℝ} (hlam : 0 < lam) (Lam : ℝ) : lambdaRef (uniformRefBlock d lam Lam) = lam / 2

theorem HCPolySupport.HighContrast.bigLambdaRef_uniformRefBlock_le {d : ℕ} {lam Lam : ℝ} (hLam : 0 ≤ Lam) : bigLambdaRef (uniformRefBlock d lam Lam) ≤ 2 * Lam

theorem HCPolySupport.HighContrast.zero_le_aspectRatio_uniformRefBlock {d : ℕ} [NeZero d] {lam : ℝ} (hlam : 0 < lam) (Lam : ℝ) : 0 ≤ aspectRatio (uniformRefBlock d lam Lam)

theorem HCPolySupport.HighContrast.aspectRatio_uniformRefBlock_le {d : ℕ} [NeZero d] {lam Lam : ℝ} (hlam : 0 < lam) (hLam : 0 ≤ Lam) : aspectRatio (uniformRefBlock d lam Lam) ≤ 4 * (Lam / lam)

The reference aspect ratio of a uniformly elliptic law: the aspect ratio Π = Λ₀/λ₀ of the diagonal reference block diag(2Λ, 2λ⁻¹) is at most 4Λ/λ.

theorem HCPolySupport.HighContrast.two_add_aspectRatio_uniformRefBlock_le {d : ℕ} [NeZero d] {lam Lam : ℝ} (hlam : 0 < lam) (hR : 1 ≤ Lam / lam) (hLam : 0 ≤ Lam) : 2 + aspectRatio (uniformRefBlock d lam Lam) * 2 ≤ (2 + Lam / lam) ^ 4

The length bound of the general theorem, read through the reference aspect ratio of a uniformly elliptic law: 2 + Π K ≤ (2 + Λ/λ)^4 at the growth witness K = 2.

Theorem t.uniform.homogenization

theorem HCPolySupport.HighContrast.uniform_homogenization_of_polynomial_homogenization (d : ℕ) (hd : 2 ≤ d) : ∃ (κ : ℝ) (C : ℝ) (C₀ : ℝ → ℝ → ℝ → ℝ) (C₁ : ℝ → ℝ), 0 < κ ∧ 0 < C ∧ (∀ (s₀ ρ Rad : ℝ), 0 < C₀ s₀ ρ Rad) ∧ (∀ (ϑ : ℝ), 0 < C₁ ϑ) ∧ ∀ (lam Lam : ℝ), 0 < lam → lam ≤ 1 → 1 ≤ Lam → ∀ (P : MeasureTheory.Measure (CoeffSpace d)), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → (∀ᵐ (a : CoeffSpace d) ∂P, ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (↑↑a x)) → ∃ (abar : Mat d) (X : CoeffSpace d → ℝ) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), 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)) ∧ (∀ (t : ℝ), 1 ≤ t → P.real {a : CoeffSpace d | C * (2 + Lam / lam) ^ C * t ≤ X a} ≤ Real.exp (-t ^ ↑d)) ∧ (∀ (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 / 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, ∀ (ε : ℝ), 0 < ε → X a ≤ ε⁻¹ → ∀ (g₀ : H1Function U), (∃ (Lg : ℝ), ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, |g₀.toFun x| + √(vecNormSq (g₀.grad x)) ≤ Lg) → hsNormSq U s₀ g₀.grad ≠ ⊤ → ∀ (h : H1Function U), MemAffineH10 U g₀ h → IsWeakSolutionOn (fun (x : Vec d) => abar) U h.grad → ⋯) ∧ (∀ 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⁻¹ * negOneNorm (ellipsoid abar r) fun (x : Vec d) => matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (↑↑a x - skewPart abar) (e + gradPhi e a x) - matVecMul (symmPart abar) e)) ≤ 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), MemLiouvilleClass (fun (x : Vec d) => ↑↑a x) ϑ v Dv → ∃ (e : Vec d) (c : ℝ), v =ᵐ[MeasureTheory.volume] fun (x : Vec d) => vecDot e x + Phi e a x + c) ∧ ∀ (e : Vec d) (c : ℝ), MemLiouvilleClass (fun (x : Vec d) => ↑↑a x) ϑ (fun (x : Vec d) => vecDot e x + Phi e a x + c) fun (x : Vec d) => e + gradPhi e a x) ∧ ∀ a ∈ Ωend, ∀ (R : ℝ), X a ≤ R → ∀ (u : Vec d → ℝ) (Du : Vec d → Vec d), MemH1a (fun (x : Vec d) => ↑↑a x) (ellipsoid abar R) u Du → IsWeakSolutionOn (fun (x : Vec d) => ↑↑a x) (ellipsoid abar R) Du → (∀ r ∈ Set.Icc (X a) R, weightedGradNorm (fun (x : Vec d) => ↑↑a x) (ellipsoid abar r) Du ≤ ENNReal.ofReal C * weightedGradNorm (fun (x : Vec d) => ↑↑a x) (ellipsoid abar R) Du) ∧ ∀ ϑ ∈ Set.Ioo 0 1, ∃ (e : Vec d), ∀ r ∈ Set.Icc (X a) R, (weightedGradNorm ⋯ (ellipsoid abar r) fun (x : Vec d) => Du x - (e + gradPhi e a x)) ≤ ENNReal.ofReal (C₁ ϑ * (r / R) ^ ϑ) * ⋯

Theorem t.uniform.homogenization: quantitative homogenization under uniform ellipticity.

For a ℤ^d-stationary law of unit range whose fields satisfy e.uniform.ellipticity with 0 < λ ≤ 1 ≤ Λ there are a homogenized matrix with positive definite symmetric part, a corrector family, and a homogenization scale X ≥ 1 whose tail is e.uniform.scale.tail: the exponent is the dimension, and the deterministic factor in front of t is a power of 2 + Λ/λ with a dimensional exponent. On one translation invariant event of full probability the Dirichlet estimate, the corrector equation and estimate, the Liouville classification, the large-scale energy estimate e.uniform.energy and the first-order approximation all hold.

The estimates are those of the general theorem t.random.homogenization, specialized at the exponent g = 0: the two-part tail collapses to exp(-t^d) because the source scale of a uniformly elliptic law vanishes, and the homogenization length L ≤ (2 + Π K)^C becomes (2 + Λ/λ)^C because the reference block diag(2Λ, 2λ⁻¹) has reference aspect ratio Π ≤ 4Λ/λ.

Scope. The Dirichlet clause is the homogeneous negative-Sobolev estimate on the adapted cells of the homogenized matrix, not the L² estimate e.uniform.dirichlet with a forcing term f on the ellipsoids e.homogenized.ellipsoids; the reference text deduces the latter from the former by a separate duality argument, which is not carried out here. The large-scale energy estimate and the first-order approximation are stated on the ellipsoids E_r of e.homogenized.ellipsoids.