The convolution walk law and the product law of the increments

Source lines 711–730 and 777–780. The statement-level object PoissonDeclumping.walkLaw μ m (Setup/Walk.lean) is the law of S_m = X_1 + ⋯ + X_m defined as an m-fold convolution of the step law on ℤ, and walkProb μ m i = Ψ_m(i) = P(S_m = i) (with Ψ_m = 0 for m < 0). The proofs about the Łukasiewicz coding work with the law Lukasiewicz.walkVecLaw μ n of the vector (X_1, …, X_n) (a product measure on Fin n → ℤ). This file proves that the two agree:

• walkLaw_eq_map_sum: walkLaw μ m is the image of walkVecLaw μ m under ω ↦ ω_1 + ⋯ + ω_m;
• walkProb_natCast, walkProb_eq_toReal_walkMass: Ψ_m(i) = P(S_m = i) computed in the product model, and as the total weight walkMass μ m i of the paths of length m ending at i;
• walkProb_neg_one: the Kemperman (Dwass) identity Ψ_n(-1) = n P(|𝒯| = n), and walkProb_neg_one_pos_iff: Ψ_n(-1) > 0 exactly at the admissible sizes;
• walkVecLaw_map_split, walkVecLaw_map_sum_castAdd: the first m and the last k increments of (X_1, …, X_{m+k}) are independent with the laws of (X_1, …, X_m) and (X_1, …, X_k); in particular S_m computed from the first m coordinates has law walkLaw μ m (finite-dimensional marginals).

The paper's sequences are indexed from 1; ours from 0.

theorem PoissonDeclumping.stepLaw_eq_toMeasure (μ : PMF ℕ) : stepLaw μ = (Lukasiewicz.stepPMF μ).toMeasure

The step law of Setup/Walk.lean is the step law of the Łukasiewicz files.

theorem PoissonDeclumping.walkLaw_eq_map_sum (μ : PMF ℕ) (m : ℕ) : walkLaw μ m = MeasureTheory.Measure.map (fun (ω : Fin m → ℤ) => ∑ i : Fin m, ω i) (Lukasiewicz.walkVecLaw μ m)

Bridge between the two walk laws. The m-fold convolution walkLaw μ m is the law of S_m = X_1 + ⋯ + X_m when (X_1, …, X_m) has the product law walkVecLaw μ m.

theorem PoissonDeclumping.walkLaw_apply (μ : PMF ℕ) (m : ℕ) (s : Set ℤ) : (walkLaw μ m) s = (Lukasiewicz.walkVecLaw μ m) {ω : Fin m → ℤ | ∑ i : Fin m, ω i ∈ s}

theorem PoissonDeclumping.walkLaw_singleton (μ : PMF ℕ) (m : ℕ) (i : ℤ) : (walkLaw μ m) {i} = (Lukasiewicz.walkVecLaw μ m) {ω : Fin m → ℤ | ∑ j : Fin m, ω j = i}

P(S_m = i) in the convolution model equals P(X_1 + ⋯ + X_m = i) in the product model.

theorem PoissonDeclumping.levelSet_admissible (n : ℕ) (s : ℤ) (x : List ℤ) : x ∈ Lukasiewicz.levelSet n s → x.length = n ∧ ∀ a ∈ x, -1 ≤ a

theorem PoissonDeclumping.ofFn_mem_levelSet_iff {n : ℕ} (s : ℤ) (ω : Fin n → ℤ) : List.ofFn ω ∈ Lukasiewicz.levelSet n s ↔ ω ∈ {ω : Fin n → ℤ | ∑ i : Fin n, ω i = s} ∧ ∀ (i : Fin n), -1 ≤ ω i

theorem PoissonDeclumping.walkVecLaw_sum_eq (μ : PMF ℕ) (n : ℕ) (s : ℤ) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | ∑ i : Fin n, ω i = s} = Lukasiewicz.walkMass μ n s

P(X_1 + ⋯ + X_n = s) is the total weight walkMass μ n s of the paths with increments ≥ -1 of length n ending at s.

theorem PoissonDeclumping.walkLaw_singleton_eq_walkMass (μ : PMF ℕ) (m : ℕ) (s : ℤ) : (walkLaw μ m) {s} = Lukasiewicz.walkMass μ m s

Ψ_m(i)

theorem PoissonDeclumping.walkProb_natCast (μ : PMF ℕ) (m : ℕ) (i : ℤ) : walkProb μ (↑m) i = (Lukasiewicz.walkVecLaw μ m).real {ω : Fin m → ℤ | ∑ j : Fin m, ω j = i}

Ψ_m(i) = P(S_m = i) for m ≥ 0, computed in the product model of (X_1, …, X_m).

theorem PoissonDeclumping.walkProb_natCast_eq_toReal (μ : PMF ℕ) (m : ℕ) (i : ℤ) : walkProb μ (↑m) i = ((walkLaw μ m) {i}).toReal

theorem PoissonDeclumping.walkProb_eq_toReal_walkMass (μ : PMF ℕ) (m : ℕ) (i : ℤ) : walkProb μ (↑m) i = (Lukasiewicz.walkMass μ m i).toReal

theorem PoissonDeclumping.walkProb_of_neg (μ : PMF ℕ) {m : ℤ} (hm : m < 0) (i : ℤ) : walkProb μ m i = 0

The paper's convention Ψ_m(i) = 0 for m < 0.

theorem PoissonDeclumping.walkProb_nonneg (μ : PMF ℕ) (m i : ℤ) : 0 ≤ walkProb μ m i

theorem PoissonDeclumping.walkProb_le_one (μ : PMF ℕ) (m i : ℤ) : walkProb μ m i ≤ 1

theorem PoissonDeclumping.walkProb_natCast_sub (μ : PMF ℕ) (n m : ℕ) (i : ℤ) : walkProb μ (↑n - ↑m) i = (if m ≤ n then (walkLaw μ (n - m)) {i} else 0).toReal

Ψ_{n-m}(i) with m, n ∈ ℕ, in ℝ≥0∞: P(S_{n-m} = i) if m ≤ n and 0 otherwise.

theorem PoissonDeclumping.walkProb_neg_one (μ : PMF ℕ) (n : ℕ) : walkProb μ (↑n) (-1) = ↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | T.vertexCount = n}

Kemperman / Dwass identity for Ψ: Ψ_n(-1) = n P(|𝒯| = n).

theorem PoissonDeclumping.walkLaw_neg_one (μ : PMF ℕ) (n : ℕ) : (walkLaw μ n) {-1} = ↑n * (PlaneTree.bienayme μ) {T : PlaneTree | T.vertexCount = n}

Ψ_n(-1) = P(S_n = -1) in ℝ≥0∞.

theorem PoissonDeclumping.not_admissible_zero (μ : PMF ℕ) : ¬PlaneTree.Admissible μ 0

No tree has 0 vertices, so 0 is never admissible.

theorem PoissonDeclumping.walkProb_neg_one_pos_iff (μ : PMF ℕ) (n : ℕ) : 0 < walkProb μ (↑n) (-1) ↔ PlaneTree.Admissible μ n

Ψ_n(-1) > 0 exactly at the admissible sizes n (P(|𝒯| = n) > 0).

Finite-dimensional marginals of the increments

theorem PoissonDeclumping.walkVecLaw_map_split (μ : PMF ℕ) (m k : ℕ) : MeasureTheory.Measure.map (fun (ω : Fin (m + k) → ℤ) => (fun (i : Fin m) => ω (Fin.castAdd k i), fun (j : Fin k) => ω (Fin.natAdd m j))) (Lukasiewicz.walkVecLaw μ (m + k)) = (Lukasiewicz.walkVecLaw μ m).prod (Lukasiewicz.walkVecLaw μ k)

Independent blocks of increments. Under the law of (X_1, …, X_{m+k}), the first m increments and the last k increments are independent, with the laws of (X_1, …, X_m) and (X_1, …, X_k).

theorem PoissonDeclumping.walkVecLaw_map_sum_castAdd (μ : PMF ℕ) (m k : ℕ) : MeasureTheory.Measure.map (fun (ω : Fin (m + k) → ℤ) => ∑ i : Fin m, ω (Fin.castAdd k i)) (Lukasiewicz.walkVecLaw μ (m + k)) = walkLaw μ m

The law of S_m = X_1 + ⋯ + X_m, computed from the first m coordinates of (X_1, …, X_{m+k}), is walkLaw μ m.

theorem PoissonDeclumping.walkVecLaw_map_sum_castLE (μ : PMF ℕ) {m n : ℕ} (h : m ≤ n) : MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => ∑ i : Fin m, ω (Fin.castLE h i)) (Lukasiewicz.walkVecLaw μ n) = walkLaw μ m

The law of S_m computed from the first m coordinates of (X_1, …, X_n), m ≤ n.

theorem PoissonDeclumping.walkVecLaw_map_sum_pair (μ : PMF ℕ) (m k : ℕ) : MeasureTheory.Measure.map (fun (ω : Fin (m + k) → ℤ) => (∑ i : Fin m, ω (Fin.castAdd k i), ∑ j : Fin k, ω (Fin.natAdd m j))) (Lukasiewicz.walkVecLaw μ (m + k)) = (walkLaw μ m).prod (walkLaw μ k)

The joint law of (S_m, S_{m+k} - S_m) is walkLaw μ m ⊗ walkLaw μ k.