Documentation

LeanPool.Superdiffusion.Algsuperdiff.Probability.RDependent

RDependent #

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

r-dependence of a ℤ-indexed family, and the ZMod (r+1) colouring #

ABK26, Proposition p.concentration, specialised to a ℤ-indexed sequence.

"Since the sequence {X_j} is 2-dependent, we may apply Proposition p.concentration …"

Why r and not 2 #

The manuscript's "2-dependent" is dimension-restricted, while the reusable predicate here records dependence at an arbitrary separation radius r.

The colouring #

Splitting a window [n, m] ⊆ ℤ into the r+1 residue classes mod r+1 makes two distinct indices of one class differ by a nonzero multiple of r+1, hence be ≥ r-separated, hence make the class mutually independent. That separation property is le_abs_sub_of_intCast_zmod_eq; the palette size is card_zmod_succ.

Main results #

References #

The r-dependence hypothesis #

source
def Algsuperdiff.Probability.RDependent {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (X : ℤ → Ω → ℝ) (r : ℕ) :
Prop

A family X : ℤ → Ω → ℝ is r-dependent: any finite set of pairwise ≥ r-separated indices is mutually independent. This is the hypothesis of ABK26 p.concentration specialised to a ℤ-indexed sequence, and the hypothesis under which Step 1 of l.minimal.scale.sep invokes it.

Equations
Instances For
    source
    theorem Algsuperdiff.Probability.RDependent.comp {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ℤ → Ω → ℝ} {r : ℕ} (h : RDependent P X r) (g : ℤ → ℝ → ℝ) (hg : ∀ (j : ℤ), Measurable (g j)) :
    RDependent P (fun (j : ℤ) (ω : Ω) => g j (X j ω)) r

    r-dependence is stable under composing each coordinate with a measurable map (used to pass from X to the centred family X − E X).

    The ZMod (r+1) colouring of a window #

    source
    theorem Algsuperdiff.Probability.le_abs_sub_of_intCast_zmod_eq {r : ℕ} {i j : ℤ} (h : ↑i = ↑j) (hij : i ≠ j) :
    ↑r + 1 ≤ |i - j|

    The colouring's separation property. Two distinct integers with the same residue mod r+1 differ by a nonzero multiple of r+1, hence by at least r+1. (For r = 2 this is "same residue mod 3 ⟹ |i − j| > 1".)

    source
    theorem Algsuperdiff.Probability.card_zmod_succ (r : ℕ) :
    ↑(Fintype.card (ZMod (r + 1))) = ↑r + 1

    The ZMod (r+1) palette has exactly r+1 colours.