High-contrast homogenization: Provider.PolynomialHomogenization.FractionalChainPhysicalHead #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.tsum_fractionalChainPhysicalHead_le
{r L D a : ℝ}
(hr : 0 < r)
(hL : 0 < L)
(hD : r < D)
(ha : 0 < a)
(P : ℕ → Prop)
[DecidablePred P]
(hP : ∀ (n : ℕ), P n → r < (1 / 2) ^ n * L)
:
(∑' (n : ℕ), if P n then ENNReal.ofReal ((2 ^ a) ^ n) else 0) ≤ ENNReal.ofReal (D ^ a) * ENNReal.ofReal (r ^ (-a)) + ENNReal.ofReal (L ^ a) * ENNReal.ofReal (r ^ (-a)) * ENNReal.ofReal (2 ^ a / (2 ^ a - 1))
A geometric chain whose level-n support lies within the physical
distance 2⁻ⁿ L has total growing weight controlled by the Riesz kernel
r⁻ᵃ, uniformly up to the explicit outer scales D and L.