High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.CorrectorEnergyOnCube

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

The corrector's own energy, in the representative form the terminal uses

The exists_scalarIdentityGoodTailJointWeightedGradientBoundConstant bounds the affine-plus-corrector energy on every cube above the good-tail start by B * euclideanNorm e, with B law-free. It is stated on the local H¹ object finiteAffineCorrectionJointLocalH1 a hCauchy e q; the large-scale C¹ slope approximation terminal speaks of fun y ↦ e + (Phi e).globalGradientRepresentative y.

The two agree a.e. on the cube — finiteAffineCorrectionJointLocalH1 is by definition the affine boundary function plus the carrier's local H¹ function, and globalGradientRepresentative_ae_eq_localH1Gradient identifies the representative with that local gradient. This module performs that one weightedGradNorm_congr_ae, for an arbitrary joint-local-equation carrier Phi (pinned to the canonical limit by isFiniteAffineCorrectionJointLocalLimit_iff_eq).

Nothing here is an estimate.

theorem HCPolySupport.HighContrast.Root.exists_jointCorrectorRepresentativeEnergyBound (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 → FiniteAffineCorrectionLocalCauchy a → ∀ (Phi : Vec d → NormalizedLocalH1Carrier d), IsFiniteAffineCorrectionJointLocalEquation a Phi → ∀ (e : Vec d) (q : ℕ), n ≤ ↑q → (weightedGradNorm (a.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) fun (y : Vec d) => e + (Phi e).globalGradientRepresentative y) ≤ ENNReal.ofReal (B * euclideanNorm e)

The corrector energy bound, in representative form. Above the good-tail start the affine-plus-corrector energy on every origin cube is at most B * euclideanNorm e, with B depending only on (d, s).