High-contrast homogenization: Provider.PolynomialHomogenization.ConvexFractionalChainMeanJumpScale

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

Scale-normalized consecutive fractional-chain mean jumps

theorem HCPolySupport.HighContrast.edist_convexFractionalChainMean_succ_le_scale_amplitude {d : ℕ} (hd : 1 ≤ 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))) ≤ convexFractionalChainJumpConstant d rho Rad s * ENNReal.ofReal (convexFractionalChainScale n ^ (s - ↑d)) * ∫⁻ (z : Vec d) in convexFractionalChainBall c x rho n, fractionalGagliardoAmplitude U s G z

Every consecutive chain-ball mean jump is bounded by a structural constant times scale^(s-d) and the amplitude mass on the level-n ball.