Reduction

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

Concentration for scale arrays — Step 1 (reduction to a counting problem)

This module formalizes Step 1 of the proof (e.YktoZk.twosided): the deterministic reduction of the weighted-row exceedance 𝟙{Y_k > 3 λ s⁻¹} to the column exceedance counts Z_j.

The paper's threshold is 2 λ s⁻¹ (from the sharp geometric constant 4/s); we use 3 λ s⁻¹ (from the clean constant 6/s), see Weights.lean.

Main results:

• sum_wt_half_le: ∑_j 3^{-(s/2)|k-j|} ≤ 6/s;
• Yk_le_of_pointwise: the pointwise implication of Step 1;
• exists_exceed_of_Yk_gt: contrapositive — a large Y_k forces a column exceedance;
• indicator_Yk_le_tsum: the pointwise ℝ≥0∞ counting bound, the row indicator 𝟙{Y_k > 3λs⁻¹} below the tsum of the column indicators;
• sum_indicator_Yk_le_tsum_Zcount: summed over k ∈ {0,…,m}.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.idist_eq (k j : ℤ) : idist k j = ↑(k - j).natAbs

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.summable_wt_half {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (k : ℤ) : Summable fun (j : ℤ) => wt (s / 2) k j

Summability of the half-weights j ↦ 3^{-(s/2)|k-j|}.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.sum_wt_half_le {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (k : ℤ) : ∑' (j : ℤ), wt (s / 2) k j ≤ 6 / s

The half-weight sum bound: ∑_j 3^{-(s/2)|k-j|} ≤ 6/s for s ∈ (0,1].

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.wt_mul_le_of_bound {Ω : Type u_1} {s lam : ℝ} (X : ℤ → ℤ → Ω → ℝ) (k j : ℤ) (ω : Ω) (hb : X k j ω ≤ thr s lam k j) : wt s k j * X k j ω ≤ lam / 2 * wt (s / 2) k j

The termwise comparison 3^{-s|k-j|} X_{k,j} ≤ (λ/2) 3^{-(s/2)|k-j|} under the columnwise threshold bound.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.summable_wt_mul_of_le {Ω : Type u_1} {s lam : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (X : ℤ → ℤ → Ω → ℝ) (k : ℤ) (ω : Ω) (hXnn : ∀ (j : ℤ), 0 ≤ X k j ω) (hbound : ∀ (j : ℤ), X k j ω ≤ thr s lam k j) : Summable fun (j : ℤ) => wt s k j * X k j ω

Summability of the weighted row when X is bounded columnwise by the Step-2 thresholds.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.Yk_le_of_pointwise {Ω : Type u_1} {s lam : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (X : ℤ → ℤ → Ω → ℝ) (k : ℤ) (ω : Ω) (hlam : 0 ≤ lam) (hXnn : ∀ (j : ℤ), 0 ≤ X k j ω) (hbound : ∀ (j : ℤ), X k j ω ≤ thr s lam k j) : Yk X s k ω ≤ 3 * lam / s

Step 1, pointwise bound. If every column at row k is below its threshold, then the weighted row Y_k is at most 3 λ s⁻¹.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.exists_exceed_of_Yk_gt {Ω : Type u_1} {s lam : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (X : ℤ → ℤ → Ω → ℝ) (k : ℤ) (ω : Ω) (hlam : 0 ≤ lam) (hXnn : ∀ (j : ℤ), 0 ≤ X k j ω) (hY : 3 * lam / s < Yk X s k ω) : ∃ (j : ℤ), thr s lam k j < X k j ω

Step 1, contrapositive. If Y_k > 3 λ s⁻¹ then some column exceeds its threshold.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.zcount_cast_eq {Ω : Type u_1} {s lam : ℝ} (X : ℤ → ℤ → Ω → ℝ) (m : ℕ) (j : ℤ) (ω : Ω) : ↑(Zcount X s lam m j ω) = ∑ k ∈ Finset.Icc 0 ↑m, if thr s lam k j < X k j ω then 1 else 0

The ℝ≥0∞-valued column count equals the cast of Zcount.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.indicator_Yk_le_tsum {Ω : Type u_1} {s lam : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (X : ℤ → ℤ → Ω → ℝ) (k : ℤ) (ω : Ω) (hlam : 0 ≤ lam) (hXnn : ∀ (j : ℤ), 0 ≤ X k j ω) : (if 3 * lam / s < Yk X s k ω then 1 else 0) ≤ ∑' (j : ℤ), if thr s lam k j < X k j ω then 1 else 0

Step 1, pointwise ℝ≥0∞ bound. The row indicator is dominated by the tsum of column indicators.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.tsum_finsetSum_swap {ι : Type u_2} (s : Finset ι) (f : ι → ℤ → ENNReal) : ∑ i ∈ s, ∑' (j : ℤ), f i j = ∑' (j : ℤ), ∑ i ∈ s, f i j

Swap a finite sum and a tsum in ℝ≥0∞ (both always defined).

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.sum_indicator_Yk_le_tsum_Zcount {Ω : Type u_1} {s lam : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (X : ℤ → ℤ → Ω → ℝ) (m : ℕ) (ω : Ω) (hlam : 0 ≤ lam) (hXnn : ∀ (k j : ℤ), 0 ≤ X k j ω) : (∑ k ∈ Finset.Icc 0 ↑m, if 3 * lam / s < Yk X s k ω then 1 else 0) ≤ ∑' (j : ℤ), ↑(Zcount X s lam m j ω)

Step 1, summed ℝ≥0∞ bound (e.YktoZk.twosided). The number of rows k ∈ {0,…,m} with Y_k > 3 λ s⁻¹ is at most ∑_j Z_j.