High-contrast homogenization: Provider.Regularity.IntrinsicSlopeTranslatedFullGradientUniqueness #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Intrinsic-slope uniqueness for a translated full gradient #
If two intrinsically normalized corrector carriers represent the same global full gradient after translating the first corrector component, the slopes are equal. The fixed-translation boundary cost is supplied by one weak corrector row for the first carrier.
theorem
HCPolySupport.HighContrast.intrinsicSlope_eq_of_translated_globalFullGradient_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)
(hGradient :
(fun (x : Vec d) => e + Phi.globalGradientRepresentative (x + t)) =ᵐ[MeasureTheory.volume] fun (x : Vec d) =>
e' + Psi.globalGradientRepresentative x)
:
A global a.e. identity between a translated full corrector gradient and an intrinsically normalized target full gradient identifies their slopes.