Tail

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

Concentration for scale arrays — Step 2 (geometric tail for Z_j)

This module formalizes the paper's Step 2 (e.Zj.tail.twosided) for a single column j: the combinatorial ⌈n/2⌉-shells argument, the per-shell Markov bound, and the union-bound + geometric-series assembly giving

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

No independence is used here.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.shell_max {j : ℤ} {d : ℕ} (E : Finset ℤ) (hne : E.Nonempty) (hE : ∀ k ∈ E, d ≤ (k - j).natAbs) (hfib : ∀ (ℓ : ℕ), {k ∈ E | (k - j).natAbs = ℓ}.card ≤ 2) {n : ℕ} (hn : n ≤ E.card) : ∃ k ∈ E, 2 * d + n ≤ 2 * (k - j).natAbs + 2

Combinatorial core of Step 2 (the ⌈n/2⌉-shells argument).

If E is a finite set of integers, each at "shell distance" ≥ d from j, with at most 2 members per shell, then having ≥ n members forces some member at shell distance ≥ d + (n-2)/2 (written 2 d + n ≤ 2·shell + 2).

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.column_markov {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {p : ℝ} (hYmeas : Measurable Y) (hmomL : ∫⁻ (ω : Ω), ENNReal.ofReal (Y ω ^ p) ∂P ≤ 1) (hp : 0 < p) {t : ℝ} (ht : 0 < t) : P {ω : Ω | t < Y ω} ≤ ENNReal.ofReal (t ^ (-p))

Per-shell Markov bound. For a nonnegative variable Y with ∫⁻ ofReal(Y^p) ≤ 1 and t > 0, P[Y > t] ≤ t^{-p}.