High-contrast homogenization: Provider.Regularity.IntrinsicSlopeTranslatedGradientCancellation

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

Corrector-gradient cancellation after translated slope identification

Once intrinsic normalization identifies the affine slopes in a translated full-gradient identity, cancellation yields the corresponding identity of the corrector gradients themselves.

theorem HCPolySupport.HighContrast.globalGradient_translate_ae_eq_of_intrinsicSlopes_of_fullGradient_ae_eq_of_weakRow {d : ℕ} [NeZero d] {e e' : Vec d} {Phi Psi : NormalizedLocalH1Carrier d} (he : HasIntrinsicNormalizedSlope e Phi) (he' : HasIntrinsicNormalizedSlope e' Psi) (t eRow : Vec d) {s : ℝ} (hs : 0 < s) (hs2 : s < 1 / 2) (q0 : ℕ) (N : ℝ) (hRow : ∀ (q : ℕ), q0 ≤ q → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) s fun (x : Vec d) => eRow + Phi.globalGradientRepresentative x) ≤ N) (hFullGradient : (fun (x : Vec d) => e + Phi.globalGradientRepresentative (x + t)) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => e' + Psi.globalGradientRepresentative x) : (fun (x : Vec d) => Phi.globalGradientRepresentative (x + t)) =ᵐ[MeasureTheory.volume] Psi.globalGradientRepresentative

Intrinsic normalization and one weak corrector row turn a translated global full-gradient identity into the translated corrector-gradient identity.