High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardCovariance

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

Integer covariance of the normalized-gauge carrier, at a real translation

The identity-gauge covariance proof compares two integer phases of one sample. In the normalized gauge an integer translation of the physical sample is a translation by the real vector L⁻¹ z, so the same comparison has to run at a real translation. Every step of the identity proof carries over unchanged except the Liouville input, which is supplied here by engine_liouville_input.

theorem HCPolySupport.HighContrast.Root.memLiouvilleClass_affineAdd_of_cubeGrowth {d : ℕ} [NeZero d] (Phi : NormalizedLocalH1Carrier d) {b : CoeffField d} (e : Vec d) (hEquation : IsWeakSolutionOn b Set.univ fun (x : Vec d) => e + Phi.globalGradientRepresentative x) (q0 : ℕ) (C : ℝ) (hC : 0 ≤ C) (hcube : ∀ (q : ℕ), q0 ≤ q → cubeLpNorm (originCube d ↑q) 2 Phi.globalValueRepresentative ≤ C * 3 ^ q) {theta : ℝ} (htheta : 0 < theta) (hb : IsAELocallyUniformlyElliptic b) : MemLiouvilleClass b theta (fun (x : Vec d) => vecDot e x + Phi.globalValueRepresentative x) fun (x : Vec d) => e + Phi.globalGradientRepresentative x

The affine-plus-corrector representative of a carrier with a correction-only cube-growth row and a global corrector equation is in the Liouville class. This is the t = 0, c = 0 case of the available translated statement, assembled from the two available untranslated rows.

theorem HCPolySupport.HighContrast.Root.pushforwardCarrier_gradient_translate_ae {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (z : Fin d → ℤ) (e : Vec d) {a : CoeffSpace d} (hsrc : RootCorrectorEvent d (normalizedSample abar hS a)) (htgt : RootCorrectorEvent d (normalizedSample abar hS (translateCoeff z a))) : (fun (x : Vec d) => (rootJointCarrier d (matVecMul (gaugeRoot abar) e) (normalizedSample abar hS a)).globalGradientRepresentative (x + matVecMul (gaugeRoot abar)⁻¹ (Source.AKL.intTranslation z))) =ᵐ[MeasureTheory.volume] (rootJointCarrier d (matVecMul (gaugeRoot abar) e) (normalizedSample abar hS (translateCoeff z a))).globalGradientRepresentative

Covariance of the normalized-gauge carrier under a real translation.

On the normalized-gauge event at a sample and at its integer translate, the selected normalized carrier of the translated sample is the L⁻¹ z-translate of the selected normalized carrier of the sample, at the pulled-back slope.

The Liouville input is engine_liouville_input; the identification is the same rootCorrectorIdentification_spec engine the identity-gauge proof uses, whose translation binder is an arbitrary real vector and whose boundary cost is the source datum's weak gradient row.