MgfProduct

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

Concentration for scale arrays — Step 4 helpers (e.full.mgf.bound)

This module collects the generic analytic and combinatorial lemmas feeding the Step-4 residue-class MGF product (full_mgf_bound, assembled in Chernoff.lean), kept free of the expZfun / ColumnsIndep machinery so they read cleanly:

• prod_add_one_le_exp_ofReal — ∏ (1 + c_i) ≤ exp(∑ c_i) in ℝ≥0∞ (sub-part (d));
• dcol and sum_three_dcol_le — the window-distance d_j and the two-sided geometric ℤ-sum ∑_{j∈[-N,N]} 3^{-(sp/2) d_j} ≤ 3(m+1) (sub-part (e));
• three_div_lam_rpow — the λ-substitution algebra (3/λ)^p = θ/K;
• er_npow — the ℝ≥0∞ rpow bridge e_r^n = (B^n)^{1/r} used by Hölder.

(d) product of 1 + c_j bounded by an exponential

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.prod_add_one_le_exp {ι : Type u_1} (s : Finset ι) (c : ι → ℝ) (hc : ∀ i ∈ s, 0 ≤ c i) : ∏ i ∈ s, (1 + c i) ≤ Real.exp (∑ i ∈ s, c i)

∏_{i∈s} (1 + c_i) ≤ exp(∑_{i∈s} c_i) for nonnegative c.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.prod_add_one_le_exp_ofReal {ι : Type u_1} (s : Finset ι) (c : ι → ℝ) (hc : ∀ i ∈ s, 0 ≤ c i) : ∏ i ∈ s, ENNReal.ofReal (1 + c i) ≤ ENNReal.ofReal (Real.exp (∑ i ∈ s, c i))

∏_{i∈s} ofReal(1 + c_i) ≤ ofReal(exp(∑_{i∈s} c_i)) for nonnegative c.

(e) window distance d_j and the two-sided geometric sum

noncomputable def Algsuperdiff.Section4.Probability.ScalesConcentration.dcol (m : ℕ) (j : ℤ) : ℕ

The distance from j to the window {0, …, m}, as a natural number (0 inside the window, j - m to the right, -j to the left).

Equations

• Algsuperdiff.Section4.Probability.ScalesConcentration.dcol m j = (max (max (j - ↑m) (-j)) 0).toNat

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.dcol_le {m : ℕ} {j k : ℤ} (hk : k ∈ Finset.Icc 0 ↑m) : dcol m j ≤ (k - j).natAbs

d_j lower-bounds the shell distance |k - j| for every k ∈ {0,…,m}.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.dcol_eq_zero_iff {m : ℕ} {j : ℤ} : dcol m j = 0 ↔ 0 ≤ j ∧ j ≤ ↑m

d_j = 0 exactly on the window {0,…,m}.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.dcol_fiber_subset {m ℓ : ℕ} (hℓ : 1 ≤ ℓ) (W : Finset ℤ) : {j ∈ W | dcol m j = ℓ} ⊆ {↑m + ↑ℓ, -↑ℓ}

For a positive distance ℓ, only j = m + ℓ or j = -ℓ reach it.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.dcol_fiber_card_le {m ℓ : ℕ} (hℓ : 1 ≤ ℓ) (W : Finset ℤ) : {j ∈ W | dcol m j = ℓ}.card ≤ 2

At most two indices reach a given positive distance ℓ.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.dcol_fiber0_card_le {m : ℕ} (W : Finset ℤ) : {j ∈ W | dcol m j = 0}.card ≤ m + 1

At most m + 1 indices reach distance 0.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.sum_dcol_geom_le {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (m N : ℕ) : ∑ j ∈ Finset.Icc (-↑N) ↑N, q ^ dcol m j ≤ ↑m + 1 + 2 * (q / (1 - q))

Two-sided geometric window sum (raw form). For q ∈ [0,1), ∑_{j∈[-N,N]} q^{d_j} ≤ (m+1) + 2 q/(1-q).

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.sum_three_dcol_le {s p : ℝ} (hsp : 1 ≤ s * p) (m N : ℕ) (hm : 1 ≤ m) : ∑ j ∈ Finset.Icc (-↑N) ↑N, 3 ^ (-(s * p / 2 * ↑(dcol m j))) ≤ 3 * (↑m + 1)

Two-sided geometric window sum (specialized). For sp ≥ 1, m ≥ 1, ∑_{j∈[-N,N]} 3^{-(sp/2) d_j} ≤ 3(m+1) (C₅ = 3).

(b/c) λ-substitution algebra and the ℝ≥0∞ rpow bridge

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.three_div_lam_rpow {K θ p : ℝ} (hK : 0 < K) (hθ : 0 < θ) (hp : 0 < p) : (3 / (3 * K ^ (1 / p) * θ ^ (-1 / p))) ^ p = θ / K

The λ-substitution (3/λ)^p = θ/K for λ = 3 K^{1/p} θ^{-1/p}.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.er_eq_B_rpow (a : ℝ) (r : ℕ) : ENNReal.ofReal (Real.exp (a / ↑r)) = ENNReal.ofReal (Real.exp a) ^ (1 / ↑r)

e_r = ofReal(exp(a/r)) = B^{1/r} with B = ofReal(exp a) in ℝ≥0∞.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.er_npow (a : ℝ) (r n : ℕ) : ENNReal.ofReal (Real.exp (a / ↑r)) ^ n = (ENNReal.ofReal (Real.exp a) ^ n) ^ (1 / ↑r)

The rpow bridge e_r^n = (B^n)^{1/r} used across the Hölder classes.