High-contrast homogenization: Provider.PolynomialHomogenization.FractionalChainGeometricHead

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

Geometric heads for the fractional pointwise chain

theorem HCPolySupport.HighContrast.tsum_geometric_of_mul_pow_lt_one_le {X q : ℝ} (hX : 0 < X) (hq : 1 < q) : (∑' (n : ℕ), if X * q ^ n < 1 then ENNReal.ofReal (q ^ n) else 0) ≤ 1 + (ENNReal.ofReal X)⁻¹ * ENNReal.ofReal (q / (q - 1))

A growing geometric sequence cut off before X q^n reaches one has mass controlled by X⁻¹.