High-contrast homogenization: Provider.Quenched.SuperGeometricTail

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

Summation of a super-geometric family of exponentials

A stretched-exponential tail whose argument grows by a fixed triadic factor at each step is summable, and its sum is dominated by twice its first term as soon as the one-step gain exceeds the logarithm of two. This is the elementary mechanism that converts the per-generation Gaussian gauge of the endgame into a single stretched-exponential bound after the union bound over generations.

theorem HCPolySupport.HighContrast.Quenched.summable_exp_neg_triadic {A nu : ℝ} (hA : 0 < A) (hnu : 0 < nu) : Summable fun (j : ℕ) => Real.exp (-(A * 3 ^ (nu * ↑j)))

The triadic super-geometric exponential family is summable.

theorem HCPolySupport.HighContrast.Quenched.tsum_exp_neg_triadic_le_two_mul {A nu : ℝ} (hA : 0 ≤ A) (hnu : 0 ≤ nu) (hthr : Real.log 2 ≤ A * (3 ^ nu - 1)) : ∑' (j : ℕ), Real.exp (-(A * 3 ^ (nu * ↑j))) ≤ 2 * Real.exp (-A)

The triadic super-geometric exponential family sums to at most twice its first term once its one-step gain exceeds the logarithm of two.

theorem HCPolySupport.HighContrast.Quenched.mul_exp_neg_le_exp_neg_half {A c : ℝ} (hc : 0 < c) (hA : 2 * Real.log c ≤ A) : c * Real.exp (-A) ≤ Real.exp (-(A / 2))

A positive multiple of an exponential is absorbed by halving its exponent once the exponent dominates twice the logarithm of the multiple.