Kemperman's formula for forests and the first-passage decomposition

Work package WP2a of the bridge plan (no toolkit). Source lines 1137–1139 and 1338–1341 (Dwass' formula for a forest of ℓ independent Bienaymé trees, used in Lemma lem:forest_estimates and in Corollary cor:consequenceS(iii)), 2250–2255 (the Markov property at the first passage time to -ℓ, proof of Lemma lem:parent(iii)).

PlaneTree.forestSizeWeight μ ℓ q (Bienayme/Basic.lean) is the total weight of the ℓ-tuples of trees with q vertices in total, i.e. P(|𝒢_ℓ| = q) for a forest 𝒢_ℓ of ℓ independent μ-Bienaymé trees, and Lukasiewicz.walkMass μ q s = P(S_q = s).

Main statements

• exists_first_sum_take_eq: discrete intermediate value property of skip-free sequences.
• card_filter_rotate_firstPassageAt (generalized cycle lemma): a sequence of q integers ≥ -1 with sum -ℓ, ℓ ≥ 1, has exactly ℓ cyclic shifts whose first passage time to -ℓ is q (FirstPassageAt ℓ).
• walkVecLaw_firstPassageAt: P((X_1..X_q) first reaches -ℓ at time q) = P(|𝒢_ℓ| = q) (forests are coded by forestSeq, a bijection onto forestSet ℓ q, forestMap_bijective).
• natCast_mul_forestSizeWeight (Kemperman's formula for forests): 1 ≤ ℓ → q P(|𝒢_ℓ| = q) = ℓ P(S_q = -ℓ); real forms natCast_mul_forestSizeWeight_toReal and forestSizeWeight_toReal_eq (P(|𝒢_ℓ| = q) = (ℓ / q) Ψ_q(-ℓ) for q ≥ 1).
• walkMass_neg_eq_sum, walkProb_neg_eq_sum (forest first-passage decomposition): Ψ_N(-ℓ) = ∑_{q ≤ N} P(|𝒢_ℓ| = q) Ψ_{N-q}(0).

The proof of Kemperman's formula is the classical one: the q cyclic shifts of (X_1..X_q) have the same law (walkVecLaw_rotate), and on {S_q = -ℓ} exactly ℓ of them are forest sequences. No criticality is assumed.

First hitting times of skip-free sequences

theorem PoissonDeclumping.Bridge.exists_first_sum_take_eq {x : List ℤ} (hx : ∀ a ∈ x, -1 ≤ a) {v : ℤ} (hv : v ≤ 0) {b : ℕ} (hb : (List.take b x).sum ≤ v) : ∃ l ≤ b, (List.take l x).sum = v ∧ ∀ l' < l, v < (List.take l' x).sum

Discrete intermediate value property. If the increments are ≥ -1, v ≤ 0 and some partial sum x_1 + ⋯ + x_b is ≤ v, then there is a first time l ≤ b with x_1 + ⋯ + x_l = v, all earlier partial sums being > v.

The generalized cycle lemma

def PoissonDeclumping.Bridge.FirstPassageAt (ℓ : ℕ) (x : List ℤ) : Prop

𝐱 has its first passage time to -ℓ at its end: x_1 + ⋯ + x_q = -ℓ (q = |𝐱|) and all proper partial sums x_1 + ⋯ + x_j, j < q, are > -ℓ.

Equations

• PoissonDeclumping.Bridge.FirstPassageAt ℓ x = (x.sum = -↑ℓ ∧ ∀ j < x.length, -↑ℓ < (List.take j x).sum)

theorem PoissonDeclumping.Bridge.rotate_forest_iff {x : List ℤ} {ℓ : ℕ} (hs : x.sum = -↑ℓ) {i : ℕ} (hi : i < x.length) : (∀ j < x.length, -↑ℓ < (List.take j (x.rotate i)).sum) ↔ (∀ (l : ℕ), i ≤ l → l < x.length → (List.take i x).sum - ↑ℓ < (List.take l x).sum) ∧ ∀ l < i, (List.take i x).sum < (List.take l x).sum

The partial sums of the rotation x.rotate i stay above -ℓ before time |x| iff i is a strict running minimum of the partial sums of x that the later partial sums (before |x|) do not undercut by ℓ or more.

theorem PoissonDeclumping.Bridge.firstPassageAt_rotate_iff {x : List ℤ} {ℓ : ℕ} (hs : x.sum = -↑ℓ) {i : ℕ} (hi : i < x.length) : FirstPassageAt ℓ (x.rotate i) ↔ (∀ (l : ℕ), i ≤ l → l < x.length → (List.take i x).sum - ↑ℓ < (List.take l x).sum) ∧ ∀ l < i, (List.take i x).sum < (List.take l x).sum

A cyclic shift of a sequence with sum -ℓ has first passage time |𝐱| to -ℓ iff the characterization of rotate_forest_iff holds.

theorem PoissonDeclumping.Bridge.card_filter_rotate_firstPassageAt {x : List ℤ} (hx : ∀ a ∈ x, -1 ≤ a) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (hs : x.sum = -↑ℓ) [DecidablePred fun (i : ℕ) => FirstPassageAt ℓ (x.rotate i)] : {i ∈ Finset.range x.length | FirstPassageAt ℓ (x.rotate i)}.card = ℓ

Generalized cycle lemma (the combinatorial core of Kemperman's formula, source lines 1137–1139). A sequence 𝐱 of integers ≥ -1 with sum -ℓ, ℓ ≥ 1, has exactly ℓ cyclic shifts 𝐱.rotate i (0 ≤ i < |𝐱|) whose first passage time to -ℓ is |𝐱|.

Forest sequences

def PoissonDeclumping.Bridge.forestSet (ℓ q : ℕ) : Set (List ℤ)

The sequences in ℤ_{≥ -1}^q whose first passage time to -ℓ is q: the DFS sequences of the forests of ℓ trees with q vertices in total.

Equations

• PoissonDeclumping.Bridge.forestSet ℓ q = {x : List ℤ | x.length = q ∧ (∀ a ∈ x, -1 ≤ a) ∧ PoissonDeclumping.Bridge.FirstPassageAt ℓ x}

theorem PoissonDeclumping.Bridge.excursion_forestSeq (ts : List PlaneTree) : (PlaneTree.forestSeq ts).sum = -↑ts.length ∧ ∀ j < (PlaneTree.forestSeq ts).length, -↑ts.length < (List.take j (PlaneTree.forestSeq ts)).sum

Excursion property of forest sequences, specialized from the common coding lemma.

theorem PoissonDeclumping.Bridge.length_forestSeq_eq_sum (ts : List PlaneTree) : (PlaneTree.forestSeq ts).length = (List.map PlaneTree.vertexCount ts).sum

theorem PoissonDeclumping.Bridge.forestSeq_injective_of_length_eq {ts us : List PlaneTree} (hl : ts.length = us.length) (h : PlaneTree.forestSeq ts = PlaneTree.forestSeq us) : ts = us

Forests with the same number of trees are determined by their DFS sequence.

theorem PoissonDeclumping.Bridge.walkWeight_forestSeq (μ : PMF ℕ) (ts : List PlaneTree) : Lukasiewicz.walkWeight μ (PlaneTree.forestSeq ts) = (List.map (PlaneTree.weight μ) ts).prod

theorem PoissonDeclumping.Bridge.forestSeq_ofFn_mem_forestSet {ℓ : ℕ} (f : Fin ℓ → PlaneTree) : PlaneTree.forestSeq (List.ofFn f) ∈ forestSet ℓ (∑ i : Fin ℓ, (f i).vertexCount)

def PoissonDeclumping.Bridge.forestMap (ℓ q : ℕ) : ↑{f : Fin ℓ → PlaneTree | ∑ i : Fin ℓ, (f i).vertexCount = q} → ↑(forestSet ℓ q)

The DFS coding of forests of ℓ trees with q vertices in total.

Equations

• PoissonDeclumping.Bridge.forestMap ℓ q f = ⟨PoissonDeclumping.PlaneTree.forestSeq (List.ofFn ↑f), ⋯⟩

theorem PoissonDeclumping.Bridge.forestMap_bijective (ℓ q : ℕ) : Function.Bijective (forestMap ℓ q)

theorem PoissonDeclumping.Bridge.forestSizeWeight_eq_tsum (μ : PMF ℕ) (ℓ q : ℕ) : PlaneTree.forestSizeWeight μ ℓ q = ∑' (x : ↑(forestSet ℓ q)), Lukasiewicz.walkWeight μ ↑x

The total weight of the forests of ℓ trees with q vertices is the total walk weight of their DFS sequences.

theorem PoissonDeclumping.Bridge.walkVecLaw_firstPassageAt (μ : PMF ℕ) (ℓ q : ℕ) : (Lukasiewicz.walkVecLaw μ q) {ω : Fin q → ℤ | FirstPassageAt ℓ (List.ofFn ω)} = PlaneTree.forestSizeWeight μ ℓ q

Forests in the walk. P((X_1, …, X_q) has first passage time qto-ℓ) = P(|𝒢_ℓ| = q), where 𝒢_ℓ is a forest of ℓ independent Bienaymé trees.

theorem PoissonDeclumping.Bridge.ae_walkVecLaw_neg_one_le (μ : PMF ℕ) (n : ℕ) : ∀ᵐ (ω : Fin n → ℤ) ∂Lukasiewicz.walkVecLaw μ n, ∀ (i : Fin n), -1 ≤ ω i

Almost surely all increments are ≥ -1.

theorem PoissonDeclumping.Bridge.natCast_mul_forestSizeWeight (μ : PMF ℕ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (q : ℕ) : ↑q * PlaneTree.forestSizeWeight μ ℓ q = ↑ℓ * Lukasiewicz.walkMass μ q (-↑ℓ)

Kemperman's formula for forests (Dwass, source lines 1137–1139, 1338–1341): for ℓ ≥ 1, q P(|𝒢_ℓ| = q) = ℓ P(S_q = -ℓ), where 𝒢_ℓ is a forest of ℓ independent Bienaymé trees.

theorem PoissonDeclumping.Bridge.forestSizeWeight_le_one (μ : PMF ℕ) (ℓ q : ℕ) : PlaneTree.forestSizeWeight μ ℓ q ≤ 1

P(|𝒢_ℓ| = q) ≤ 1.

theorem PoissonDeclumping.Bridge.forestSizeWeight_ne_top (μ : PMF ℕ) (ℓ q : ℕ) : PlaneTree.forestSizeWeight μ ℓ q ≠ ⊤

theorem PoissonDeclumping.Bridge.natCast_mul_forestSizeWeight_toReal (μ : PMF ℕ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (q : ℕ) : ↑q * (PlaneTree.forestSizeWeight μ ℓ q).toReal = ↑ℓ * walkProb μ (↑q) (-↑ℓ)

Kemperman's formula for forests, with Ψ: q P(|𝒢_ℓ| = q) = ℓ Ψ_q(-ℓ).

theorem PoissonDeclumping.Bridge.forestSizeWeight_toReal_eq (μ : PMF ℕ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) {q : ℕ} (hq : 1 ≤ q) : (PlaneTree.forestSizeWeight μ ℓ q).toReal = ↑ℓ / ↑q * walkProb μ (↑q) (-↑ℓ)

Kemperman's formula for forests, the paper's form (source line 1138): P(|𝒢_ℓ| = q) = (ℓ / q) P(S_q = -ℓ) for q ≥ 1.

The first-passage decomposition at level -ℓ

theorem PoissonDeclumping.Bridge.firstPassageAt_take_unique {x : List ℤ} {ℓ q q' : ℕ} (hq : q ≤ x.length) (hq' : q' ≤ x.length) (h : FirstPassageAt ℓ (List.take q x)) (h' : FirstPassageAt ℓ (List.take q' x)) : q = q'

The first passage time to -ℓ is unique: if both (x_1, …, x_q) and (x_1, …, x_{q'}) have their first passage time to -ℓ at their end, then q = q' (for q, q' ≤ |𝐱|).

theorem PoissonDeclumping.Bridge.walkMass_neg_eq_sum (μ : PMF ℕ) (ℓ N : ℕ) : Lukasiewicz.walkMass μ N (-↑ℓ) = ∑ q ∈ Finset.range (N + 1), PlaneTree.forestSizeWeight μ ℓ q * Lukasiewicz.walkMass μ (N - q) 0

Forest first-passage decomposition (source lines 2250–2255): decomposing according to the first passage time q of the walk to -ℓ (the size of the forest of the first ℓ trees), Ψ_N(-ℓ) = ∑_{q ≤ N} P(|𝒢_ℓ| = q) Ψ_{N-q}(0).

theorem PoissonDeclumping.Bridge.walkProb_neg_eq_sum (μ : PMF ℕ) (ℓ N : ℕ) : walkProb μ (↑N) (-↑ℓ) = ∑ q ∈ Finset.range (N + 1), (PlaneTree.forestSizeWeight μ ℓ q).toReal * walkProb μ (↑(N - q)) 0

Forest first-passage decomposition, with Ψ (source lines 2250–2255): Ψ_N(-ℓ) = ∑_{q ≤ N} P(|𝒢_ℓ| = q) Ψ_{N-q}(0).