The excursion law

Let μ be an offspring probability measure and n a size. The offspring counts ω : Fin n → ℕ under Measure.pi (fun _ => μ) have a Łukasiewicz step word stepWord ω; it is a tree excursion exactly when ω lies in countExcursions n, the event {ζ(X) = n} that the walk first reaches -1 at time n. The excursion law is the law of the counts given this event.

• pi_countExcursions: P(ζ(X) = n) = P(|T| = n), the mass of countExcursions n is the mass of the size event under the Bienaymé–Galton–Watson law;
• the excursion law is a probability measure exactly at admissible sizes (pi_countExcursions_ne_zero_iff), and is the zero measure otherwise;
• the atom of the excursion law at the count vector of the code of a tree t of size n is the atom of t in the size-conditioned law (cond_pi_countExcursions_singleton_code), and vanishes off countExcursions n;
• for every set A of count vectors, the excursion mass of A is the expectation over a tree t drawn from the size-conditioned law of the indicator of A at the count vector of its code (cond_pi_countExcursions_apply_eq_tsum): the code of the conditioned tree has the excursion law.

As for the cyclic shift in BridgeLaw, this is stated without a measure on finite trees, which carry no measurable structure here. No criticality, aperiodicity or positivity hypothesis is made; both sides vanish at inadmissible sizes and at n = 0. Adapted from PoissonDeclumping/Lukasiewicz/BridgeLaw.lean (map_dfsSeq_conditioned, excursionLaw, walkVecLaw_zeta_eq_bienayme). Local limit theorems are not part of this module.

def BGW.countExcursions (n : ℕ) : Set (Fin n → ℕ)

The offspring-count vectors whose step word is a tree excursion: the Łukasiewicz walk first reaches -1 at time n.

Equations

• BGW.countExcursions n = {ω : Fin n → ℕ | BGW.IsTreeExcursion (BGW.stepWord ω)}

theorem BGW.stepWord_mem_excursions_iff {n : ℕ} (ω : Fin n → ℕ) : stepWord ω ∈ {x : List ℤ | IsTreeExcursion x ∧ x.length = n} ↔ ω ∈ countExcursions n

A count vector has a tree excursion as step word iff it lies in countExcursions n.

theorem BGW.tsum_excursions_walkWeight (p : ℕ → ENNReal) (n : ℕ) : ∑' (x : List ℤ), {x : List ℤ | IsTreeExcursion x ∧ x.length = n}.indicator (walkWeight p) x = ∑' (ω : Fin n → ℕ), (countExcursions n).indicator (fun (ω : Fin n → ℕ) => ∏ i : Fin n, p (ω i)) ω

Reindexing the tree excursions of length n by offspring-count vectors.

theorem BGW.pi_countExcursions (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ) (countExcursions n) = (LocallyFinite.bienaymeLaw μ) (LocallyFinite.sizeEvent n)

P(ζ(X) = n) = P(|T| = n): the first passage of the walk to -1 at time n has the mass of the size event.

theorem BGW.pi_countExcursions_ne_zero_iff (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ) (countExcursions n) ≠ 0 ↔ (LocallyFinite.bienaymeLaw μ) (LocallyFinite.sizeEvent n) ≠ 0

The excursion event has positive mass iff the size n is admissible.

theorem BGW.isProbabilityMeasure_cond_pi_countExcursions (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (h : (LocallyFinite.bienaymeLaw μ) (LocallyFinite.sizeEvent n) ≠ 0) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi fun (x : Fin n) => μ)[|countExcursions n]

At an admissible size, the excursion law is a probability measure.

theorem BGW.cond_pi_countExcursions_eq_zero (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (h : (LocallyFinite.bienaymeLaw μ) (LocallyFinite.sizeEvent n) = 0) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ)[|countExcursions n] = 0

At an inadmissible size, the excursion law is the zero measure.

theorem BGW.cond_pi_countExcursions_singleton (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (ω : Fin n → ℕ) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ)[{ω} | countExcursions n] = (countExcursions n).indicator (fun (ω : Fin n → ℕ) => (∏ i : Fin n, μ {ω i}) / (MeasureTheory.Measure.pi fun (x : Fin n) => μ) (countExcursions n)) ω

The atoms of the excursion law: the point masses of the excursion count vectors divided by the mass of the excursion event.

theorem BGW.stepWord_countsOfWord_increments {n : ℕ} (t : PlaneTree) (ht : t.size = n) : stepWord (countsOfWord n t.increments) = t.increments

Decoding the code of a tree of size n to counts and re-encoding returns the code.

theorem BGW.cond_pi_countExcursions_singleton_code (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (t : PlaneTree) (ht : t.size = n) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ)[{countsOfWord n t.increments} | countExcursions n] = (LocallyFinite.bienaymeLaw μ)[{t.toLocallyFinite} | LocallyFinite.sizeEvent n]

Excursion law, atoms. The atom of the excursion law at the count vector of the code of a tree t of size n is the atom of t in the size-conditioned law.

theorem BGW.cond_pi_countExcursions_apply_eq_tsum (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Set (Fin n → ℕ)) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ)[A | countExcursions n] = ∑' (t : { t : PlaneTree // t.size = n }), (LocallyFinite.bienaymeLaw μ)[{(↑t).toLocallyFinite} | LocallyFinite.sizeEvent n] * A.indicator 1 (countsOfWord n (↑t).increments)

Excursion law, law. For every set A of count vectors, the excursion mass of A is the expectation, over a tree t drawn from the size-conditioned law, of the indicator of A at the count vector of the code of t: the code of the size-conditioned tree has the excursion law.