High-contrast homogenization: Provider.Regularity.CorrectorLiouvilleForward

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

Forward Liouville inclusion for intrinsic affine correctors

This module assembles the local Sobolev representative, global weak equation, and best-fit-normalized growth chain into the forward inclusion of the frozen Liouville classification. Only the local Sobolev clause reads the coefficient field.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.tendsto_affineAdd_normalizedL2Norm_sublinear_of_cubeGrowth {d : ℕ} [NeZero d] (z : NormalizedLocalH1Carrier d) (q₀ : ℕ) (C : ℝ) (hC : 0 ≤ C) (hcube : ∀ (q : ℕ), q₀ ≤ q → cubeLpNorm (originCube d ↑q) 2 z.globalValueRepresentative ≤ C * 3 ^ q) (e : Vec d) (c : ℝ) {ϑ : ℝ} (hϑ : 0 < ϑ) : Filter.Tendsto (fun (r : ℝ) => ENNReal.ofReal (r ^ (-(1 + ϑ))) * normalizedL2Norm (euclideanBall d r) fun (x : Vec d) => vecDot e x + z.globalValueRepresentative x + c) Filter.atTop (nhds 0)

Correction-only cube growth implies the exact frozen sublinear limit for every affine-plus-corrector representative and every additive constant.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailAffineCorrectorSublinearGrowthConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (K : ℝ) (c : ℝ), 0 < K ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (c₀ ϑ : ℝ), 0 < ϑ → Filter.Tendsto (fun (r : ℝ) => ENNReal.ofReal (r ^ (-(1 + ϑ))) * normalizedL2Norm (euclideanBall d r) fun (x : Vec d) => vecDot e x + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalValueRepresentative x + c₀) Filter.atTop (nhds 0)

A scalar intrinsic good tail therefore gives the frozen sublinear-growth condition for every affine-plus-corrector representative.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailAffineCorrectorMemLiouvilleConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (K : ℝ) (c : ℝ), 0 < K ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∀ {b : CoeffField d}, IsAELocallyUniformlyElliptic b → (∀ (q : ℕ), Book.Ch03.publicCoeffField (originCube d ↑q) a =ᵐ[volumeMeasureOn (localGradientCube d q)] b) → ∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (c₀ ϑ : ℝ), 0 < ϑ → MemLiouvilleClass b ϑ (fun (x : Vec d) => vecDot e x + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalValueRepresentative x + c₀) fun (x : Vec d) => e + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalGradientRepresentative x

The intrinsic affine corrector belongs to the exact frozen Liouville class. This is the forward inclusion, including arbitrary additive constants.