High-contrast homogenization: Provider.Regularity.CorrectorJointGoodTailEquation

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

Fixed-cube equations for joint corrector limits

A sufficiently small scalar good tail gives a unique family of normalized local finite-corrector limits. On every fixed centered cube, adding the affine boundary function to the corresponding local representative gives a coefficient-harmonic gradient.

theorem HCPolySupport.HighContrast.exists_finiteAffineCorrectionJointLocalEquationGoodTailThreshold (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ c ∈ Set.Ioo 0 1, ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∃! Phi : Vec d → NormalizedLocalH1Carrier d, (∀ (e : Vec d), IsNormalizedLocalLimit (finiteAffineCorrectionLocalSequence a e) (Phi e)) ∧ ∀ (e : Vec d) (q : ℕ), IsAHarmonicGradient (a.coeffOn (originCube d ↑q)).toCoeffField (localGradientCube d q) ((have this := id (finiteAffineBoundaryH1 (↑q) e); this) + (Phi e).localH1Function q).grad

Below a dimension-and-exponent threshold, a scalar good tail determines one unique joint normalized local limit whose affine extensions are coefficient-harmonic on every fixed centered cube.