The conditional bridge law and the uniform cyclic shift

Let μ be an offspring probability measure and n a size. The conditional bridge law is the law of the offspring counts ω : Fin n → ℕ under Measure.pi (fun _ => μ) given the bridge event countBridges n = {S_n = -1}. It is a probability measure exactly when n ≠ 0 and the size n is admissible (pi_countBridges_ne_zero_iff); in the other cases it is the zero measure.

The cyclic-shift representation says that the Łukasiewicz code of the size-conditioned tree, rotated by an independent uniform index of Fin n, has the conditional bridge law. It is stated without a measure on finite trees, which carry no measurable structure here. The atom of the bridge law at the count vector of a rotation of the code of a tree t of size n is n⁻¹ times the atom of t in the size-conditioned law (cond_pi_countBridges_singleton_shift). For every set A of count vectors, the conditional bridge mass is the expectation, over a tree t drawn from the conditioned law and a uniform index i, of the indicator of A at the count vector of the i-th rotation of the code of t (cond_pi_countBridges_apply_eq_tsum). The proof uses the shift equivalence of the cycle lemma, which makes the pairs (t, i) and the bridge words correspond exactly once, and the rotation invariance of the walk weight. No criticality, aperiodicity or positivity hypothesis is made; both sides vanish at inadmissible sizes. countsOfWord n is a left inverse of stepWord, and a two-sided inverse on words of length n with entries at least -1. Adapted from PoissonDeclumping/Lukasiewicz/BridgeLaw.lean (map_shift_conditioned). The excursion law, local limit theorems and the passage to the limit are not part of this module.

def BGW.countsOfWord (n : ℕ) (x : List ℤ) : Fin n → ℕ

The offspring counts x i + 1 read off a word: a left inverse of stepWord, and a two-sided inverse on words of length n with entries at least -1.

Equations

• BGW.countsOfWord n x i = (x.getD (↑i) 0 + 1).toNat

theorem BGW.countsOfWord_stepWord {n : ℕ} (ω : Fin n → ℕ) : countsOfWord n (stepWord ω) = ω

theorem BGW.stepWord_countsOfWord {n : ℕ} {x : List ℤ} (hlen : x.length = n) (hge : ∀ a ∈ x, -1 ≤ a) : stepWord (countsOfWord n x) = x

theorem BGW.tsum_bridgeWords_walkWeight_mul (p : ℕ → ENNReal) (n : ℕ) (g : List ℤ → ENNReal) : ∑' (x : List ℤ), (bridgeWords n).indicator (fun (x : List ℤ) => walkWeight p x * g x) x = ∑' (ω : Fin n → ℕ), (countBridges n).indicator (fun (ω : Fin n → ℕ) => (∏ i : Fin n, p (ω i)) * g (stepWord ω)) ω

Reindexing the bridge words, with a test function of the word, by offspring-count vectors.

theorem BGW.tsum_shift_weight_mul (p : ℕ → ENNReal) (n : ℕ) (g : List ℤ → ENNReal) : ∑' (q : { t : PlaneTree // t.size = n } × Fin n), PlaneTree.weight p ↑q.1 * g ((↑q.1).increments.rotate ↑q.2) = ∑' (x : List ℤ), (bridgeWords n).indicator (fun (x : List ℤ) => walkWeight p x * g x) x

The pairs (tree of size n, rotation index) cover the bridge words exactly once, with the weight of the tree equal to the walk weight of the rotated code.

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

The bridge event has positive mass iff n ≠ 0 and the size n is admissible.

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

At an admissible size n ≠ 0, the conditional bridge law is a probability measure.

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

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

theorem BGW.cond_pi_countBridges_singleton_shift (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (t : PlaneTree) (ht : t.size = n) (i : Fin n) (ω : Fin n → ℕ) (hω : stepWord ω = t.increments.rotate ↑i) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ)[{ω} | countBridges n] = (↑n)⁻¹ * (LocallyFinite.bienaymeLaw μ)[{t.toLocallyFinite} | LocallyFinite.sizeEvent n]

Uniform cyclic shift, atoms. If the code of a tree t of size n, rotated by i, is the step word of the count vector ω, then the atom of ω in the conditional bridge law is n⁻¹ times the atom of t in the size-conditioned law.

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

Uniform cyclic shift, law. For every set A of count vectors, the conditional bridge mass of A is the expectation over t drawn from the size-conditioned law and an independent uniform index i of Fin n (n⁻¹ per index) of the indicator of A at the count vector of the i-th rotation of the code of t.