High-contrast homogenization: Provider.PolynomialHomogenization.FractionalChainTonelli

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

Tonelli aggregation for the infinite fractional chain

theorem HCPolySupport.HighContrast.ofReal_convexFractionalChainScale_rpow_sub_eq (d n : ℕ) (s : ℝ) : ENNReal.ofReal (convexFractionalChainScale n ^ (s - ↑d)) = ENNReal.ofReal ((2 ^ (↑d - s)) ^ n)

The negative dyadic scale power is the growing geometric weight used in the physical chain-head estimate.

theorem HCPolySupport.HighContrast.tsum_scaleWeight_mul_setLIntegral_chainBall_eq {d : ℕ} {c x : Vec d} {rho s : ℝ} {A : Vec d → ENNReal} (hA : Measurable A) : ∑' (n : ℕ), ENNReal.ofReal (convexFractionalChainScale n ^ (s - ↑d)) * ∫⁻ (y : Vec d) in convexFractionalChainBall c x rho n, A y = ∫⁻ (y : Vec d), ∑' (n : ℕ), (convexFractionalChainBall c x rho n).indicator (fun (y : Vec d) => ENNReal.ofReal (convexFractionalChainScale n ^ (s - ↑d)) * A y) y

Tonelli exchanges the sum of weighted amplitude masses on the chain balls with the spatial integral of the pointwise chain-membership weight.