High-contrast homogenization: Provider.PolynomialHomogenization.ConvexFractionalChainMeanTelescope

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

Telescoping means on the infinite convex fractional chain

noncomputable def HCPolySupport.HighContrast.convexFractionalChainMean {d : ℕ} (c x : Vec d) (rho : ℝ) (F : Vec d → Vec d) (n : ℕ) : Vec d

The volume average on the level-n ball of the infinite convex chain.

Equations

• HCPolySupport.HighContrast.convexFractionalChainMean c x rho F n = HCPolySupport.volumeAverageVec (HCPolySupport.HighContrast.convexFractionalChainBall c x rho n) F

theorem HCPolySupport.HighContrast.convexFractionalChainMean_zero {d : ℕ} (c x : Vec d) (rho : ℝ) (F : Vec d → Vec d) : convexFractionalChainMean c x rho F 0 = volumeAverageVec (euclideanBallAt c rho) F

theorem HCPolySupport.HighContrast.edist_convexFractionalChainMean_zero_le_tsum_jumps {d : ℕ} {c x : Vec d} {rho : ℝ} {F : Vec d → Vec d} (hmean : Filter.Tendsto (fun (n : ℕ) => HilbertVec.ofVec (convexFractionalChainMean c x rho F n)) Filter.atTop (nhds (HilbertVec.ofVec (F x)))) : edist (HilbertVec.ofVec (convexFractionalChainMean c x rho F 0)) (HilbertVec.ofVec (F x)) ≤ ∑' (n : ℕ), edist (HilbertVec.ofVec (convexFractionalChainMean c x rho F n)) (HilbertVec.ofVec (convexFractionalChainMean c x rho F (n + 1)))

Once the shrinking chain-ball means converge to the endpoint value, their distance from the core-ball mean is bounded by the sum of all successive mean jumps.