High-contrast homogenization:

Provider.PolynomialHomogenization.ConvexFractionalChainMeanJumpAmplitude

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

Consecutive convex-chain mean jumps against the Gagliardo amplitude

theorem HCPolySupport.HighContrast.edist_convexFractionalChainMean_succ_le_amplitude {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {c x : Vec d} {rho Rad s : ℝ} (hrho : 0 < rho) (hRad : 0 ≤ Rad) (hinner : euclideanBallAt c rho ⊆ U) (houter : U ⊆ euclideanBallAt c Rad) (hx : x ∈ U) {G : Vec d → Vec d} (hGmeas : Measurable G) (hGint : MeasureTheory.Integrable G (MeasureTheory.volume.restrict U)) (hs : 0 ≤ ↑d + 2 * s) (n : ℕ) : edist (HilbertVec.ofVec (convexFractionalChainMean c x rho G n)) (HilbertVec.ofVec (convexFractionalChainMean c x rho G (n + 1))) ≤ (MeasureTheory.volume (convexFractionalChainBall c x rho (n + 1)))⁻¹ * (MeasureTheory.volume (convexFractionalChainBall c x rho (n + 1)) * ENNReal.ofReal ((3 / 2 * convexFractionalChainScale n * (Rad + rho)) ^ (↑d + 2 * s))) ^ (1 / 2) * (MeasureTheory.volume (convexFractionalChainBall c x rho n))⁻¹ * ∫⁻ (z : Vec d) in convexFractionalChainBall c x rho n, fractionalGagliardoAmplitude U s G z

A consecutive jump of chain-ball means is controlled by the integral of the global Gagliardo amplitude on the larger ball, with exact geometric and volume factors.