Excursions, the first-passage decomposition, and weighted cyclic-shift identities

Complements to PoissonDeclumping.Lukasiewicz.CyclicShift, at the level of weights.

• Lukasiewicz.excursionSet n: sequences in ℤ_{≥ -1}^n with first passage time ζ = n. 𝐱 is a bijection from trees with n vertices onto it (PlaneTree.dfsEquiv); in weights, the DFS sequence of 𝒯^n has the law of (X_1, …, X_n) given ζ(𝐗) = n (first half of eq:shifts, source lines 726–727; PlaneTree.tsum_weight_mul_dfsSeq).
• Lukasiewicz.levelSet n s: sequences in ℤ_{≥ -1}^n with sum s, and Lukasiewicz.walkMass μ n s = ∑_{𝐲 ∈ levelSet n s} ∏ μ_{y_i + 1}, i.e. Ψ_n(s) = P(S_n = s) for the walk with step law P(X = i) = μ_{i+1}.
• The first-passage decomposition of a bridge: a bridge 𝐱 ∈ ℤ_{≥ -1}^n with sum -1 splits uniquely as 𝐱(T) 𝐲 with |T| ≤ n and 𝐲 ∈ ℤ_{≥ -1}^{n - |T|} of sum 0 (PlaneTree.appendEquiv); this is the Markov property at ζ used in the proof of Corollary cor:cyclicshift (source lines 811–825).
• PlaneTree.tsum_sum_weight_mul_fringe: the weighted form of Corollary cor:cyclicshift, ∑_{|T| = n} P_μ(T) ∑_{i < n} G(T_{u_i}) = E[G(𝒯) Ψ_{n - |𝒯|}(0)] (with the convention Ψ_{n-m}(0) = 0 for m > n); dividing by n P(|𝒯| = n) = Ψ_n(-1) gives the corollary.

def PoissonDeclumping.Lukasiewicz.excursionSet (n : ℕ) : Set (List ℤ)

The sequences in ℤ_{≥ -1}^n whose first passage time to -1 is n.

Equations

• PoissonDeclumping.Lukasiewicz.excursionSet n = {x : List ℤ | x.length = n ∧ (∀ a ∈ x, -1 ≤ a) ∧ PoissonDeclumping.Lukasiewicz.zeta x = some n}

def PoissonDeclumping.Lukasiewicz.levelSet (n : ℕ) (s : ℤ) : Set (List ℤ)

The sequences in ℤ_{≥ -1}^n with sum s.

Equations

• PoissonDeclumping.Lukasiewicz.levelSet n s = {x : List ℤ | x.length = n ∧ (∀ a ∈ x, -1 ≤ a) ∧ x.sum = s}

theorem PoissonDeclumping.Lukasiewicz.bridgeSet_eq_levelSet (n : ℕ) : bridgeSet n = levelSet n (-1)

noncomputable def PoissonDeclumping.Lukasiewicz.walkWeight (μ : PMF ℕ) (x : List ℤ) : ENNReal

The weight P(X_1 = x_1, …, X_n = x_n) = ∏ μ_{x_i + 1} of a sequence with entries ≥ -1.

Equations

• PoissonDeclumping.Lukasiewicz.walkWeight μ x = (List.map (fun (a : ℤ) => μ (a + 1).toNat) x).prod

noncomputable def PoissonDeclumping.Lukasiewicz.walkMass (μ : PMF ℕ) (n : ℕ) (s : ℤ) : ENNReal

Ψ_n(s) = P(S_n = s): the total walk weight of levelSet n s.

Equations

• PoissonDeclumping.Lukasiewicz.walkMass μ n s = ∑' (x : ↑(PoissonDeclumping.Lukasiewicz.levelSet n s)), PoissonDeclumping.Lukasiewicz.walkWeight μ ↑x

theorem PoissonDeclumping.Lukasiewicz.walkWeight_append (μ : PMF ℕ) (x y : List ℤ) : walkWeight μ (x ++ y) = walkWeight μ x * walkWeight μ y

theorem PoissonDeclumping.Lukasiewicz.excursionSet_subset_bridgeSet (n : ℕ) : excursionSet n ⊆ bridgeSet n

theorem PoissonDeclumping.Lukasiewicz.exists_zeta_eq_of_mem_bridgeSet {n : ℕ} {x : List ℤ} (hx : x ∈ bridgeSet n) : ∃ (m : ℕ), zeta x = some m ∧ m ≤ n

Every bridge sequence has a finite first passage time to -1, at most its length.

theorem PoissonDeclumping.PlaneTree.weight_eq_walkWeight (μ : PMF ℕ) (T : PlaneTree) : weight μ T = Lukasiewicz.walkWeight μ T.dfsSeq

The DFS sequence of a tree with n vertices

theorem PoissonDeclumping.PlaneTree.dfsSeq_mem_excursionSet (T : PlaneTree) : T.dfsSeq ∈ Lukasiewicz.excursionSet T.vertexCount

def PoissonDeclumping.PlaneTree.dfsMap (n : ℕ) : { T : PlaneTree // T.vertexCount = n } → ↑(Lukasiewicz.excursionSet n)

The DFS coding of trees with n vertices.

Equations

• PoissonDeclumping.PlaneTree.dfsMap n T = ⟨(↑T).dfsSeq, ⋯⟩

theorem PoissonDeclumping.PlaneTree.dfsMap_bijective (n : ℕ) : Function.Bijective (dfsMap n)

noncomputable def PoissonDeclumping.PlaneTree.dfsEquiv (n : ℕ) : { T : PlaneTree // T.vertexCount = n } ≃ ↑(Lukasiewicz.excursionSet n)

Łukasiewicz bijection. Trees with n vertices correspond to the sequences in ℤ_{≥ -1}^n with first passage time ζ = n.

Equations

• PoissonDeclumping.PlaneTree.dfsEquiv n = Equiv.ofBijective (PoissonDeclumping.PlaneTree.dfsMap n) ⋯

theorem PoissonDeclumping.PlaneTree.tsum_weight_mul_dfsSeq (μ : PMF ℕ) (n : ℕ) (g : List ℤ → ENNReal) : ∑' (T : { T : PlaneTree // T.vertexCount = n }), weight μ ↑T * g (↑T).dfsSeq = ∑' (x : ↑(Lukasiewicz.excursionSet n)), Lukasiewicz.walkWeight μ ↑x * g ↑x

DFS law of 𝒯^n, weighted form. Summing P_μ(T) g(𝐱(T)) over trees with n vertices gives the sum of P(X_1 = x_1, …, X_n = x_n) g(𝐱) over {ζ = n}.

First-passage decomposition of bridges

def PoissonDeclumping.PlaneTree.appendMap (n : ℕ) : (T : { T : PlaneTree // T.vertexCount ≤ n }) × ↑(Lukasiewicz.levelSet (n - (↑T).vertexCount) 0) → ↑(Lukasiewicz.bridgeSet n)

(T, 𝐲) ↦ 𝐱(T) 𝐲, from trees with at most n vertices and sequences in ℤ_{≥ -1}^{n - |T|} with sum 0, to bridges of length n.

Equations

• PoissonDeclumping.PlaneTree.appendMap n p = ⟨(↑p.fst).dfsSeq ++ ↑p.snd, ⋯⟩

@[simp]

theorem PoissonDeclumping.PlaneTree.coe_appendMap (n : ℕ) (p : (T : { T : PlaneTree // T.vertexCount ≤ n }) × ↑(Lukasiewicz.levelSet (n - (↑T).vertexCount) 0)) : ↑(appendMap n p) = (↑p.fst).dfsSeq ++ ↑p.snd

theorem PoissonDeclumping.PlaneTree.appendMap_bijective (n : ℕ) : Function.Bijective (appendMap n)

noncomputable def PoissonDeclumping.PlaneTree.appendEquiv (n : ℕ) : (T : { T : PlaneTree // T.vertexCount ≤ n }) × ↑(Lukasiewicz.levelSet (n - (↑T).vertexCount) 0) ≃ ↑(Lukasiewicz.bridgeSet n)

First-passage decomposition (Markov property at ζ): bridges of length n correspond to pairs (T, 𝐲) with |T| ≤ n and 𝐲 ∈ ℤ_{≥ -1}^{n - |T|} of sum 0, via 𝐱(T) 𝐲.

Equations

• PoissonDeclumping.PlaneTree.appendEquiv n = Equiv.ofBijective (PoissonDeclumping.PlaneTree.appendMap n) ⋯

theorem PoissonDeclumping.PlaneTree.tsum_bridge_mul_ofSeq (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → ENNReal) : ∑' (x : ↑(Lukasiewicz.bridgeSet n)), Lukasiewicz.walkWeight μ ↑x * (ofSeq ↑x).elim 0 G = ∑' (T : PlaneTree), if T.vertexCount ≤ n then weight μ T * G T * Lukasiewicz.walkMass μ (n - T.vertexCount) 0 else 0

Markov property at ζ, weighted form. For every G, the bridge sum of P(𝐗 = 𝐱) G(T(𝐱)) equals E[G(𝒯) Ψ_{n - |𝒯|}(0)] in weights, with Ψ_{n-m}(0) = 0 for m > n.

theorem PoissonDeclumping.PlaneTree.natCast_mul_tsum_weight_eq_walkMass (μ : PMF ℕ) (n : ℕ) : (↑n * ∑' (T : PlaneTree), if T.vertexCount = n then weight μ T else 0) = Lukasiewicz.walkMass μ n (-1)

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

theorem PoissonDeclumping.PlaneTree.tsum_sum_weight_mul_fringe (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → ENNReal) : ∑' (T : { T : PlaneTree // T.vertexCount = n }), ∑ i : Fin n, weight μ ↑T * G (↑T).fringeTrees[↑i] = ∑' (T : PlaneTree), if T.vertexCount ≤ n then weight μ T * G T * Lukasiewicz.walkMass μ (n - T.vertexCount) 0 else 0

Weighted form of Corollary cor:cyclicshift. For every G, ∑_{|T| = n} P_μ(T) ∑_{i < n} G(T_{u_i}) = ∑_{|T| ≤ n} P_μ(T) G(T) Ψ_{n - |T|}(0). Dividing by n P(|𝒯| = n) = Ψ_n(-1) (natCast_mul_tsum_weight_eq_walkMass) gives E[G(𝒯^n_{U_n})] = E[G(𝒯) Ψ_{n - |𝒯|}(0)] / Ψ_n(-1).