The scalar walk on one product probability space

The product law of the increments is the coordinatewise image of independent offspring counts. Its sum has the convolution law. Prefix and suffix events are independent, with all split-time bounds explicit.

Adapted from PoissonDeclumping/Cyclic/WalkBridge.lean, PoissonDeclumping/Bridge/WalkCalculus.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0).

noncomputable def BGW.StableTrees.Scalar.walkVecLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure (Fin n → ℤ)

The product law of n independent increments with law stepLaw μ.

Equations

• BGW.StableTrees.Scalar.walkVecLaw μ n = MeasureTheory.Measure.pi fun (x : Fin n) => BGW.StableTrees.stepLaw μ

instance BGW.StableTrees.Scalar.instIsProbabilityMeasureForallFinIntWalkVecLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (walkVecLaw μ n)

theorem BGW.StableTrees.Scalar.walkVecLaw_singleton (μ : PMF ℕ) (n : ℕ) (ω : Fin n → ℤ) : (walkVecLaw μ n) {ω} = ∏ i : Fin n, (stepLaw μ) {ω i}

theorem BGW.StableTrees.Scalar.map_offspring_pi (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure.map (fun (ω : Fin n → ℕ) (i : Fin n) => ↑(ω i) - 1) (MeasureTheory.Measure.pi fun (x : Fin n) => μ.toMeasure) = walkVecLaw μ n

Mapping each offspring count to K - 1 gives the product increment law.

theorem BGW.StableTrees.Scalar.walkLaw_eq_map_sum (μ : PMF ℕ) (m : ℕ) : walkLaw μ m = MeasureTheory.Measure.map (fun (ω : Fin m → ℤ) => ∑ i : Fin m, ω i) (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 BGW.StableTrees.Scalar.walkLaw_apply (μ : PMF ℕ) (m : ℕ) (s : Set ℤ) : (walkLaw μ m) s = (walkVecLaw μ m) {ω : Fin m → ℤ | ∑ i : Fin m, ω i ∈ s}

theorem BGW.StableTrees.Scalar.walkLaw_eq_map_offspring_sum (μ : PMF ℕ) (n : ℕ) : walkLaw μ n = MeasureTheory.Measure.map (fun (ω : Fin n → ℕ) => ∑ i : Fin n, (↑(ω i) - 1)) (MeasureTheory.Measure.pi fun (x : Fin n) => μ.toMeasure)

The convolution walk law is also the image of the original offspring-count product.

theorem BGW.StableTrees.Scalar.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))) (walkVecLaw μ (m + k)) = (walkVecLaw μ m).prod (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 BGW.StableTrees.Scalar.walkVecLaw_take_inter_drop (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H K : List ℤ → Prop) : (walkVecLaw μ n) {ω : Fin n → ℤ | H (List.take m (List.ofFn ω)) ∧ K (List.drop m (List.ofFn ω))} = (walkVecLaw μ m) {a : Fin m → ℤ | H (List.ofFn a)} * (walkVecLaw μ (n - m)) {b : Fin (n - m) → ℤ | K (List.ofFn b)}

Independence of a prefix block and the following increments: P(H(X_1..X_m), K(X_{m+1}..X_n)) = P(H(X_1..X_m)) P(K(X_1..X_{n-m})).

theorem BGW.StableTrees.Scalar.walkVecLaw_take (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H : List ℤ → Prop) : (walkVecLaw μ n) {ω : Fin n → ℤ | H (List.take m (List.ofFn ω))} = (walkVecLaw μ m) {a : Fin m → ℤ | H (List.ofFn a)}

A prefix has the product law of the corresponding length.