GeometricSums

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

Geometric closures for the minimal-scale separation window sums

ABK26, l.minimal.scale.sep Steps 1--3. This module collects the deterministic geometric-series arithmetic those three steps consume, all of it carrier-free.

The three series

• ∑_r 3^{−αr} = (1 − 3^{−α})⁻¹ — the plain closure constant geomTailConst α;
• ∑_r (r+1) 3^{−αr} = (1 − 3^{−α})⁻² — the linear-weight closure;
• ∑_r √(r+1) 3^{−αr} ≤ (1 − 3^{−α})^{−3/2} — the sharp √-weight closure geomSqrtConst α, obtained by Cauchy--Schwarz against the first two.

The crude √(r+1) ≤ r+1 gives only (1 − 3^{−α})^{−2}, half a power of α worse, which does not close the printed Step-3 envelope.

The min companion of the window rearrangement

min_div_le_sqrt_mul_rpow (min{N,C}/N ≤ √C · N^{−1/2}) is the inequality that turns the sharp min{m − n + 1, Cgeo} coefficient of Algsuperdiff.Probability.window_geom_tail_rearrange into the printed (m − n)^{−1/2} envelope, at cost Cgeo^{3/2} rather than Cgeo². Without the min the Step-1 envelope fails at m − n = 1 by a power of the parameter.

Also here

The one-sided/two-sided O_{Γ_σ} dictionary for nonnegative variables lets a one-sided geometric tail closure feed a two-sided Cesàro engine.

Main results

• Algsuperdiff.Probability.min_div_le_sqrt_mul_rpow
• Algsuperdiff.Probability.geomTailConst, Algsuperdiff.Probability.geomSqrtConst
• Algsuperdiff.Probability.sum_threePow_neg_sqrt_le
• Algsuperdiff.Probability.tsum_threePow_neg_sqrt_le

References

• ABK26, l.minimal.scale.sep, Steps 1--3 (the ℓ² ↪ ℓ¹ step).

The min companion of the window rearrangement

theorem Algsuperdiff.Probability.min_div_le_sqrt_mul_rpow {N C : ℝ} (hN : 0 < N) (hC : 0 < C) : 1 / N * min N C ≤ √C * N ^ (-1 / 2)

min{N, C}/N ≤ √C · N^{−1/2} for N > 0, C > 0 — the sharp form of the inner window-sum bound that Step 1 needs, and the inequality that makes the printed envelope close on the nose (see the module docstring).

The geometric closure constant

noncomputable def Algsuperdiff.Probability.geomTailConst (α : ℝ) : ℝ

The geometric closure constant (1 − 3^{−α})⁻¹ of the layer tail.

Equations

• Algsuperdiff.Probability.geomTailConst α = (1 - 3 ^ (-α))⁻¹

theorem Algsuperdiff.Probability.three_rpow_neg_lt_one {α : ℝ} (hα : 0 < α) : 3 ^ (-α) < 1

theorem Algsuperdiff.Probability.one_sub_three_rpow_neg_pos {α : ℝ} (hα : 0 < α) : 0 < 1 - 3 ^ (-α)

theorem Algsuperdiff.Probability.geomTailConst_pos {α : ℝ} (hα : 0 < α) : 0 < geomTailConst α

IsBigO ↔ IsBigOWith for nonnegative variables

IsBigO μ Ψ X A is by definition IsBigOWith μ Ψ |X| A, so for a nonnegative X the two coincide. This is what lets a one-sided geometric tail closure (one-sided precisely because it needs no summability) feed the two-sided Cesàro engine.

theorem Algsuperdiff.Probability.isBigO_iff_isBigOWith_of_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {Ψ : ℝ → ℝ} {A : ℝ} (h0 : ∀ (ω : Ω), 0 ≤ X ω) : HCPolySupport.IndependentSums.IsBigO μ Ψ X A ↔ HCPolySupport.IndependentSums.IsBigOWith μ Ψ X A

For a nonnegative variable, the one-sided and two-sided weak-Orlicz relations agree.

theorem Algsuperdiff.Probability.isBigO_of_isBigOWith_of_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {Ψ : ℝ → ℝ} {A : ℝ} (h0 : ∀ (ω : Ω), 0 ≤ X ω) (h : HCPolySupport.IndependentSums.IsBigOWith μ Ψ X A) : HCPolySupport.IndependentSums.IsBigO μ Ψ X A

theorem Algsuperdiff.Probability.isBigOWith_of_isBigO_of_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {Ψ : ℝ → ℝ} {A : ℝ} (h0 : ∀ (ω : Ω), 0 ≤ X ω) (h : HCPolySupport.IndependentSums.IsBigO μ Ψ X A) : HCPolySupport.IndependentSums.IsBigOWith μ Ψ X A

theorem Algsuperdiff.Probability.isBigO_gammaSigma_of_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {σ A : ℝ} (hA : 0 ≤ A) (hX : ∀ (ω : Ω), X ω = 0) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma σ) X A

A variable that vanishes identically is O_{Γ_σ} at every nonnegative scale — used for the empty-window layers.

Elementary √ bookkeeping

theorem Algsuperdiff.Probability.sqrt_le_self_of_one_le {x : ℝ} (hx : 1 ≤ x) : √x ≤ x

√x ≤ x for x ≥ 1.

theorem Algsuperdiff.Probability.sqrt_add_le_add_sqrt {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : √(a + b) ≤ √a + √b

Subadditivity of √ on nonnegative reals.

Reindexing a Finset.Icc sum by its offset

theorem Algsuperdiff.Probability.sum_Icc_eq_sum_range_offset (i m : ℤ) (w : ℤ → ℝ) : ∑ k ∈ Finset.Icc i m, w k = ∑ r ∈ Finset.range (m - i + 1).toNat, w (i + ↑r)

∑_{k=i}^m w k = ∑_{r < (m−i+1)⁺} w (i+r) — the offset reindexing that turns every layer window sum into a Finset.range sum, where the geometric series live. No hypothesis relating i and m is needed: for m < i both sides are empty sums.

The three geometric series

theorem Algsuperdiff.Probability.hasSum_threePow_neg {α : ℝ} (hα : 0 < α) : HasSum (fun (r : ℕ) => 3 ^ (-(α * ↑r))) (geomTailConst α)

∑'_r 3^{−αr} = (1 − 3^{−α})⁻¹, as a HasSum.

theorem Algsuperdiff.Probability.hasSum_threePow_neg_succ {α : ℝ} (hα : 0 < α) : HasSum (fun (r : ℕ) => 3 ^ (-(α * ↑r)) * (↑r + 1)) (geomTailConst α ^ 2)

∑'_r (r+1) 3^{−αr} = (1 − 3^{−α})⁻², as a HasSum.

theorem Algsuperdiff.Probability.sum_threePow_neg_le {α : ℝ} (hα : 0 < α) (s : Finset ℕ) : ∑ r ∈ s, 3 ^ (-(α * ↑r)) ≤ geomTailConst α

Every partial geometric sum is below the closure constant.

theorem Algsuperdiff.Probability.sum_threePow_neg_succ_le {α : ℝ} (hα : 0 < α) (s : Finset ℕ) : ∑ r ∈ s, 3 ^ (-(α * ↑r)) * (↑r + 1) ≤ geomTailConst α ^ 2

Every partial (r+1)-weighted geometric sum is below the squared closure constant.

noncomputable def Algsuperdiff.Probability.geomSqrtConst (α : ℝ) : ℝ

The sharp √-weighted geometric closure constant (1−3^{−α})^{−3/2}. The crude √(r+1) ≤ r+1 would give (1−3^{−α})^{−2} ≍ α^{−2}, half a power of α worse, and not enough for the printed Step-3 envelope.

Equations

• Algsuperdiff.Probability.geomSqrtConst α = √(Algsuperdiff.Probability.geomTailConst α ^ 3)

theorem Algsuperdiff.Probability.geomSqrtConst_pos {α : ℝ} (hα : 0 < α) : 0 < geomSqrtConst α

theorem Algsuperdiff.Probability.sum_threePow_neg_sqrt_le {α : ℝ} (hα : 0 < α) (s : Finset ℕ) : ∑ r ∈ s, 3 ^ (-(α * ↑r)) * √(↑r + 1) ≤ geomSqrtConst α

∑_r √(r+1) 3^{−αr} ≤ (1−3^{−α})^{−3/2}, by Cauchy--Schwarz against the pure geometric series ∑ 3^{−αr} = (1−3^{−α})⁻¹ and the linear one ∑ (r+1)3^{−αr} = (1−3^{−α})⁻². Stated for an arbitrary finite index set, so it also bounds the tsum.

theorem Algsuperdiff.Probability.summable_threePow_neg_sqrt {α : ℝ} (hα : 0 < α) : Summable fun (r : ℕ) => 3 ^ (-(α * ↑r)) * √(↑r + 1)

The √-weighted geometric series is summable.

theorem Algsuperdiff.Probability.tsum_threePow_neg_sqrt_le {α : ℝ} (hα : 0 < α) : ∑' (r : ℕ), 3 ^ (-(α * ↑r)) * √(↑r + 1) ≤ geomSqrtConst α

The tsum form of the sharp √-weighted closure.