GeometricSums

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The geometric-sum toolkit of ABK26, Section 3.1

Sums of the shape ∑_{j = n + 1}^{m} 3 ^ (2 gamma j) occur throughout ABK26. The paper introduces the constant

K_gamma = 2 (log 3) / (1 - 3 ^ (-2 gamma))

so that 2 (log 3) ∑_{j = n + 1}^{m} 3 ^ (2 gamma j) equals K_gamma (3 ^ (2 gamma m) - 3 ^ (2 gamma n)), and records the two-sided bound 0 ≤ K_gamma - gamma⁻¹ ≤ 4 together with the partial-sum estimates that follow from it.

Everything here is stated for an abstract real parameter gamma; no part of the probabilistic model is involved.

Main definitions

• Kgamma: the constant K_gamma of e.K.cgamma.def.

Main results

• two_mul_log_three_mul_sum_Ioc_rpow: the sum identity e.K.cgamma.sum.identity.
• le_Kgamma, Kgamma_le: the two halves of the estimate e.K.cgamma.ineq, gamma⁻¹ ≤ K_gamma ≤ gamma⁻¹ + 4.
• geo_part_sum, geo_part_sum_le_min_inv: the partial-sum bound e.geo.part.sum, with an explicit constant 7 in the coarse form.

References

• ABK26.

noncomputable def Algsuperdiff.Section3.Provider.Stream.Kgamma (gamma : ℝ) : ℝ

The geometric-sum constant K_gamma of ABK26, equation e.K.cgamma.def.

Equations

• Algsuperdiff.Section3.Provider.Stream.Kgamma gamma = 2 * Real.log 3 / (1 - 3 ^ (-(2 * gamma)))

theorem Algsuperdiff.Section3.Provider.Stream.Kgamma_eq (gamma : ℝ) : Kgamma gamma = 2 * Real.log 3 / (1 - 3 ^ (-(2 * gamma)))

The defining formula for Kgamma.

theorem Algsuperdiff.Section3.Provider.Stream.Kgamma_pos {gamma : ℝ} (hgamma : 0 < gamma) : 0 < Kgamma gamma

Kgamma is positive for positive gamma.

theorem Algsuperdiff.Section3.Provider.Stream.le_Kgamma {gamma : ℝ} (hgamma : 0 < gamma) : gamma⁻¹ ≤ Kgamma gamma

The lower half of ABK26's e.K.cgamma.ineq.

theorem Algsuperdiff.Section3.Provider.Stream.Kgamma_le_inv_add_two_mul_log {gamma : ℝ} (hgamma : 0 < gamma) : Kgamma gamma ≤ gamma⁻¹ + 2 * Real.log 3

The sharp form of the upper half of e.K.cgamma.ineq.

theorem Algsuperdiff.Section3.Provider.Stream.Kgamma_le {gamma : ℝ} (hgamma : 0 < gamma) : Kgamma gamma ≤ gamma⁻¹ + 4

The upper half of ABK26's e.K.cgamma.ineq with the paper's constant.

theorem Algsuperdiff.Section3.Provider.Stream.two_mul_log_three_mul_sum_Ioc_rpow {gamma : ℝ} (hgamma : 0 < gamma) {n m : ℤ} (hnm : n ≤ m) : 2 * Real.log 3 * ∑ j ∈ Finset.Ioc n m, 3 ^ (2 * gamma * ↑j) = Kgamma gamma * (3 ^ (2 * gamma * ↑m) - 3 ^ (2 * gamma * ↑n))

ABK26's e.K.cgamma.sum.identity.

theorem Algsuperdiff.Section3.Provider.Stream.geo_part_sum {gamma : ℝ} (hgamma : 0 < gamma) {n m : ℤ} (hnm : n ≤ m) : 2 * Real.log 3 * ∑ j ∈ Finset.Ioc n m, 3 ^ (2 * gamma * ↑j) ≤ min (Kgamma gamma) (2 * Real.log 3 * (↑m - ↑n)) * 3 ^ (2 * gamma * ↑m)

ABK26's e.geo.part.sum, first inequality.

theorem Algsuperdiff.Section3.Provider.Stream.geo_part_sum_le_min_inv {gamma : ℝ} (hgamma : 0 < gamma) (hquarter : gamma ≤ 1 / 4) {n m : ℤ} (hnm : n ≤ m) : 2 * Real.log 3 * ∑ j ∈ Finset.Ioc n m, 3 ^ (2 * gamma * ↑j) ≤ 7 * min gamma⁻¹ (↑m - ↑n) * 3 ^ (2 * gamma * ↑m)

ABK26's e.geo.part.sum, second inequality, with the explicit constant 7.