High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.BallTriangle

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

ExactRootBallTriangle, proved

Exactly one analytic hypothesis stands between this module and a hypothesis-free statement: the weighted-energy triangle inequality on the exact-root pullback ball, for the two fields the large-scale C¹ slope approximation terminal compares. This module discharges it.

HCPoly.Provider.PolynomialHomogenization.Root.CorrectorComposition.BallTriangleCore supplies Minkowski for ‖s^{1/2} ·‖_{L_underlined²(U)} on an arbitrary measurable set of finite volume, for two square-integrable fields and an almost everywhere elliptic coefficient. Three obligations remain, and this module proves them for the exact instance.

1. The coefficient. bRef = affineCoefficient q _ ⇑(normalizedCenteredCoeff a abar hS).1 is exactly the representative of the affinePullbackCoeffSpace q _ (normalizedCenteredCoeff a abar hS) (affinePullbackCoeffSpace_ae), whose CoeffSpace membership is the almost-everywhere ellipticity, and whose representative is strongly measurable because it is the coercion of an AEEqFun.
2. The solution's pullback gradient. MemH1a on a bounded set gives IntegrableOn (vecNormSq ∘ Du) (integrableOn_vecNormSq_grad_of_memH1a_class — the ellipsoid is bounded), hence MemVectorL2 (ellipsoid abar R) Du; the invertible pullback carries it to matImage q⁻¹ (ellipsoid abar R) = closedNormBall d R, and composing with the constant matrix q is a continuous linear map.
3. The affine-plus-corrector field. The global gradient representative of a NormalizedLocalH1Carrier is square-integrable on every exhaustion cube (memLp_globalGradientRepresentative), and the closed ball sits inside one of them (closedNormBall_subset_outerCube); the constant slope e is square-integrable because the ball has finite volume.

No hypothesis on R is needed: R ≤ 0 is covered because the two measure facts used are the finiteness of the ball's volume — true for every R — and the null case, which weightedGradNorm_of_volume_eq_zero closes with no ellipticity at all.

Square integrability of the two fields

theorem HCPolySupport.HighContrast.CorrectorComposition.memVectorL2_grad_of_memH1a {d : ℕ} {U : Set (Vec d)} {b : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (hUb : Bornology.IsBounded U) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemH1a b U u Du) : MemVectorL2 U Du

The gradient slot of an H¹_a(U) pair on a bounded U has an honest vector-valued L² realization. The H¹_{a,0} analogue is (memVectorL2_grad_of_memH1a0); this is the same argument with the bounded-U integrability lemma of the wider class.

theorem HCPolySupport.HighContrast.CorrectorComposition.memVectorL2_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : MemVectorL2 (matImage L⁻¹ U) fun (y : Vec d) => f (matVecMul L y)

Square integrability of a vector field is carried by an invertible linear pullback. Scalar version as memL2On_affinePullback; the proof is the same, the codomain playing no role.

theorem HCPolySupport.HighContrast.CorrectorComposition.memVectorL2_matVecMul {d : ℕ} {U : Set (Vec d)} (L : Mat d) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : MemVectorL2 U fun (y : Vec d) => matVecMul L (f y)

A constant matrix acts on square-integrable fields.

The two measure facts on the closed ball, at an arbitrary radius

theorem HCPolySupport.HighContrast.CorrectorComposition.measurableSet_closedNormBall (d : ℕ) (R : ℝ) : MeasurableSet (closedNormBall d R)

The closed pullback ball is measurable: it is a sublevel set of the continuous vecNormSq.

theorem HCPolySupport.HighContrast.CorrectorComposition.volume_closedNormBall_ne_top' {d : ℕ} (R : ℝ) : MeasureTheory.volume (closedNormBall d R) ≠ ⊤

The closed pullback ball has finite volume at every real radius.

theorem HCPolySupport.HighContrast.CorrectorComposition.exists_closedNormBall_subset_localGradientCube (d : ℕ) (R : ℝ) : ∃ (n : ℕ), closedNormBall d R ⊆ localGradientCube d n

The closed pullback ball at an arbitrary radius sits inside one member of the centered cube exhaustion.

Obligation 2: the solution's exact-root pullback gradient

theorem HCPolySupport.HighContrast.CorrectorComposition.memVectorL2_pullbackGrad_closedNormBall {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (a : CoeffSpace d) (R : ℝ) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemH1a (↑↑a) (ellipsoid abar R) u Du) : MemVectorL2 (closedNormBall d R) fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (Du (matVecMul (Selection.normalizedRoot (symmPart abar)) y))

The exact-root pullback of an H¹_a(E_R) gradient is square-integrable on the closed pullback ball.

Obligation 3: the affine-plus-corrector field

theorem HCPolySupport.HighContrast.CorrectorComposition.memVectorL2_affineCorrector_closedNormBall {d : ℕ} (z : NormalizedLocalH1Carrier d) (e : Vec d) (R : ℝ) : MemVectorL2 (closedNormBall d R) fun (y : Vec d) => e + z.globalGradientRepresentative y

An affine slope plus the global gradient representative of a normalized local H¹ carrier is square-integrable on the closed pullback ball.

The residue, discharged

theorem HCPolySupport.HighContrast.CorrectorComposition.exactRootBallTriangle (d : ℕ) [NeZero d] : ExactRootBallTriangle d

The weighted-energy triangle inequality on the exact-root pullback ball, for exactly the two fields the large-scale C¹ slope approximation terminal compares. This is the sole hypothesis of exactRootGaugeTerminal_onReconciled_of_ballTriangle.