High-contrast homogenization: Provider.Regularity.CorrectorIntrinsicGrowthGoodTail

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

Sub-exponential growth of the canonical corrector

A sufficiently small scalar good tail gives a scale-uniform weighted-gradient bound for the canonical affine-plus-corrector limit. Consequently that full gradient has sub-eta growth for every positive eta.

noncomputable def HCPolySupport.HighContrast.finiteAffineGrowthApproximation {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (q k : ℕ) : H1Function (localGradientCube d q)

The local H¹ approximation obtained by adding the affine function of slope e to the normalized finite corrector at scale q + k.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailJointWeightedGradientBoundConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (B : ℝ) (c : ℝ), 0 < B ∧ 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) (q : ℕ), n ≤ ↑q → weightedGradNorm (a.coeffOn (originCube d ↑q)).toCoeffField (localGradientCube d q) (finiteAffineCorrectionJointLocalH1 a hCauchy e q).grad ≤ ENNReal.ofReal (B * euclideanNorm e)

A sufficiently small scalar good tail gives a scale-uniform weighted gradient bound for the canonical affine-plus-corrector limit beyond the starting scale.