TailAssembly

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

Concentration for scale arrays — Step 2 assembly (e.Zj.tail.twosided)

This module assembles the geometric tail bound for a single column count Z_j from the two kernels proved in Tail.lean (shell_max, column_markov):

P[Z_j ≥ n] ≤ C₂ (2/λ)^p 3^{-(sp/2) d_j} 3^{-(sp/4)(n-2)₊} (Zj_tail),

for n ≥ 1, where d_j = dist(j, {0,…,m}) enters through the hypothesis hdj : ∀ k ∈ Icc 0 m, d_j ≤ |k-j|. The proof is a finite union bound over the "exceeding" rows (measure_biUnion_finset_le), per-row Markov (column_markov), and the geometric regrouping of shells (geom_shell_sum, using the ≤ 2 members per shell from shell_max's hypothesis).

The moment input is the honest lintegral form hmomL : ∫⁻ ofReal((X k j)^p) ≤ 1, exactly what column_markov consumes.

No independence is used here.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.fiber_card_le_two (S : Finset ℤ) (j : ℤ) (ℓ : ℕ) : {k ∈ S | (k - j).natAbs = ℓ}.card ≤ 2

At most two integers k sit at a given shell distance ℓ from j (namely j ± ℓ).

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.geom_shell_sum {j : ℤ} {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (K : Finset ℤ) (hfib : ∀ (ℓ : ℕ), {k ∈ K | (k - j).natAbs = ℓ}.card ≤ 2) (L₀ : ℕ) (hL : ∀ k ∈ K, L₀ ≤ (k - j).natAbs) : ∑ k ∈ K, q ^ (k - j).natAbs ≤ 2 * q ^ L₀ / (1 - q)

Geometric shell regrouping. For q ∈ [0,1), a finite set K of integers with at most two members per shell (hfib) and all shells ≥ L₀ (hL), the sum ∑_{k∈K} q^{|k-j|} is at most 2 q^{L₀}/(1-q).

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.Zj_tail {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ℤ → ℤ → Ω → ℝ} {s p lam : ℝ} (hs : 0 < s) (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) (n : ℕ) (hn : 1 ≤ n) : P {ω : Ω | n ≤ Zcount X s lam m j ω} ≤ ENNReal.ofReal (C₂ * (2 / lam) ^ p * 3 ^ (-(s * p / 2 * ↑dj)) * 3 ^ (-(s * p / 4 * max (↑n - 2) 0)))

Step 2 tail bound (e.Zj.tail.twosided). For a single column j and n ≥ 1, P[Z_j ≥ n] ≤ C₂ (2/λ)^p 3^{-(sp/2) d_j} 3^{-(sp/4)(n-2)₊}.