Geometric cover and Gaussian decay

Arbitrarily high polynomial decay absorbs the geometric growth of the spatial covering multiplicity.

theorem ESS.uc_geometric_gaussian_term_le (K b r : ℝ) (N n : ℕ) (hK : 0 ≤ K) (hb : 0 < b) (hr : 0 < r) (hN : 0 < N) : K ^ (n + 1) * Real.exp (-(b / (3 / 5 * (3 / 4) ^ n * r ^ 2))) ≤ K * (↑N * (3 / 5) / b) ^ N * r ^ (2 * N) * (K * (3 / 4) ^ N) ^ n

Each geometric-slab Gaussian term is bounded by a geometric series times a high power of the original radius.

theorem ESS.uc_geometric_gaussian_series_le (K b r : ℝ) (N : ℕ) (hK : 0 ≤ K) (hb : 0 < b) (hr : 0 < r) (hN : 0 < N) (hq : K * (3 / 4) ^ N < 1) : (Summable fun (n : ℕ) => K ^ (n + 1) * Real.exp (-(b / (3 / 5 * (3 / 4) ^ n * r ^ 2)))) ∧ ∑' (n : ℕ), K ^ (n + 1) * Real.exp (-(b / (3 / 5 * (3 / 4) ^ n * r ^ 2))) ≤ K * (↑N * (3 / 5) / b) ^ N * r ^ (2 * N) * (1 - K * (3 / 4) ^ N)⁻¹

When the polynomial order absorbs the covering multiplicity, the Gaussian slab bounds form a summable series.

theorem ESS.uc_geometric_gaussian_order (K : ℝ) (hK : 0 < K) (m : ℕ) : ∃ (N : ℕ), m + 1 ≤ N ∧ K * (3 / 4) ^ N < 1

Every desired vanishing order admits a polynomial exponent that also absorbs the fixed covering multiplicity.