High-contrast homogenization: Provider.Regularity.IntrinsicSlopeTranslationStability

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

Intrinsic-slope stability under a fixed translation

The average of a fixed translate of the global corrector gradient differs asymptotically negligibly from the unshifted average. Consequently, any carrier whose canonical global representative is that translate inherits the same intrinsic normalized slope.

theorem HCPolySupport.HighContrast.HasIntrinsicNormalizedSlope.tendsto_integral_globalGradient_translate_zero_of_weakRow {d : ℕ} [NeZero d] {e : Vec d} {Phi : NormalizedLocalH1Carrier d} (hPhi : HasIntrinsicNormalizedSlope e Phi) (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) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Vec d), Phi.globalGradientRepresentative (x + t) ∂normalizedCubeMeasure (originCube d ↑n)) Filter.atTop (nhds 0)

A fixed translate of an intrinsically normalized corrector gradient has vanishing centered normalized cube average under one weak corrector row.