High-contrast homogenization: Provider.Regularity.CorrectorIntrinsicCubeGrowth

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

Centered-cube corrector growth from an intrinsic good tail

This module packages the complete discrete-radius function-growth estimate: the coarse-grained Poincare inequality at a good scale, the anchored mean telescope, and the fluctuation-plus-mean split of the normalized norm. No representative of the physical coefficient field enters it.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailCorrectorCubeGrowthConstant (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 ≤ C ∧ ∀ (q : ℕ), n.toNat ≤ q → cubeLpNorm (originCube d ↑q) 2 (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalValueRepresentative ≤ C * 3 ^ q

A sufficiently small scalar good tail gives scale-linear normalized L² growth of the global corrector representative on all sufficiently large centered triadic cubes.