Mgf

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

Concentration for scale arrays — Step 3 (integer exponential moment)

This module assembles the per-column exponential-moment bound (e.Zj.mgf.twosided)

E[e^{a Z_j}] ≤ 1 + C₃ (3/λ)^p 3^{-(sp/2) d_j}, a = ⅛ (log 3) sp = mgfRate s p,

from the Step-2 geometric tail (Zj_tail). Because Z_j ≤ m+1 is bounded, the layer-cake sum is finite; the exponential moment is realized in ℝ≥0∞ as ∫⁻ (ofReal(e^a))^{Z_j}, the exact quantity that enters expZfun.

The proof: pointwise B^{Z} ≤ ∑_{n=0}^{N}(if n ≤ Z then B^n else 0) (single term domination), integrate to 1 + ∑_{n=1}^{N} B^n P[Z ≥ n], insert the tail, and sum the resulting geometric series (mgf_series_bound). The constant works out to C₂(1 + (1-3^{-1/8})⁻¹) ≤ C₃, folding (2·3^{s/4})^p ≤ 3^p.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.geom_natsub_sum {ρ : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (N : ℕ) (hN : 1 ≤ N) : ∑ n ∈ Finset.Icc 1 N, ρ ^ (n - 2) ≤ 1 + (1 - ρ)⁻¹

Geometric sum with a truncated (ℕ) shift: ∑_{n=1}^N ρ^{n-2} ≤ 1 + (1-ρ)⁻¹.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.two_mul_rpow_quarter_le {s : ℝ} (hs1 : s ≤ 1) : 2 * 3 ^ (s / 4) ≤ 3

The key numeric fact 2·3^{s/4} ≤ 3 for s ≤ 1.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.mgf_series_bound {s p : ℝ} (hsp : 1 ≤ s * p) (N : ℕ) (hN : 1 ≤ N) : ∑ n ∈ Finset.Icc 1 N, Real.exp (mgfRate s p) ^ n * 3 ^ (-(s * p / 4 * max (↑n - 2) 0)) ≤ 3 ^ (s * p / 4) * (1 + (1 - 3 ^ (-(1 / 8)))⁻¹)

Step-3 series bound. ∑_{n=1}^N e^{a n} 3^{-(sp/4)(n-2)₊} ≤ 3^{sp/4}(1+(1-3^{-1/8})⁻¹).

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.Zj_mgf {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ℤ → ℤ → Ω → ℝ} {s p lam : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hp : 1 ≤ p) (hsp : 1 ≤ s * p) (hlam : 0 < lam) (hXmeas : ∀ (k j : ℤ), Measurable (X k j)) (hmomL : ∀ (k j : ℤ), ∫⁻ (ω : Ω), ENNReal.ofReal (X k j ω ^ p) ∂P ≤ 1) (m : ℕ) (j : ℤ) (dj : ℕ) (hdj : ∀ k ∈ Finset.Icc 0 ↑m, dj ≤ (k - j).natAbs) : ∫⁻ (ω : Ω), ENNReal.ofReal (Real.exp (mgfRate s p)) ^ Zcount X s lam m j ω ∂P ≤ ENNReal.ofReal (1 + C₃ * (3 / lam) ^ p * 3 ^ (-(s * p / 2 * ↑dj)))

Step 3 exponential moment (e.Zj.mgf.twosided). ∫⁻ (ofReal(e^a))^{Z_j} ≤ ofReal(1 + C₃(3/λ)^p 3^{-(sp/2)d_j}).