Cyclic shifts of DFS sequences and the walk bridge

The combinatorial core of eq:shifts (source lines 718–730), as used in Lemma lem:RW and Corollary cor:cyclicshift (source lines 751–831).

• Lukasiewicz.bridgeSet n is the set of sequences (x_1, …, x_n) of integers ≥ -1 with x_1 + ⋯ + x_n = -1, i.e. the possible values of (X_1, …, X_n) on {S_n = -1}. It is finite (Lukasiewicz.bridgeSet_finite), and so is the set of trees with n vertices (PlaneTree.finite_vertexCount_eq).
• (T, i) ↦ 𝐱^{(i)}(T), the i-th cyclic shift of the DFS sequence, is a bijection from {trees with n vertices} × {0, …, n-1} onto bridgeSet n (PlaneTree.shiftEquiv), by the cycle lemma and the Łukasiewicz coding.
• The Bienaymé weight of T is the product of the step masses μ_{x+1} along any cyclic shift of 𝐱(T) (PlaneTree.weight_eq_prod_rotate), which gives the weighted form of eq:shifts (PlaneTree.tsum_sum_weight_mul_rotate) and the Kemperman/Dwass identity n · P(|𝒯| = n) = P(S_n = -1) (PlaneTree.natCast_mul_tsum_weight_eq).

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

The sequences (x_1, …, x_n) ∈ ℤ_{≥ -1}^n with x_1 + ⋯ + x_n = -1.

Equations

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

theorem PoissonDeclumping.Lukasiewicz.finite_length_eq_of_mem {s : Set ℤ} (hs : s.Finite) (n : ℕ) : {x : List ℤ | x.length = n ∧ ∀ a ∈ x, a ∈ s}.Finite

Lists of a fixed length with entries in a finite set form a finite set.

theorem PoissonDeclumping.Lukasiewicz.le_of_mem_bridgeSet {n : ℕ} {x : List ℤ} (hx : x ∈ bridgeSet n) {a : ℤ} (ha : a ∈ x) : a ≤ ↑n

Every entry of a bridge sequence of length n is at most n.

theorem PoissonDeclumping.Lukasiewicz.bridgeSet_finite (n : ℕ) : (bridgeSet n).Finite

instance PoissonDeclumping.Lukasiewicz.instFiniteElemListIntBridgeSet (n : ℕ) : Finite ↑(bridgeSet n)

theorem PoissonDeclumping.Lukasiewicz.one_le_of_mem_bridgeSet {n : ℕ} {x : List ℤ} (hx : x ∈ bridgeSet n) : 1 ≤ n

theorem PoissonDeclumping.Lukasiewicz.rotate_rotate_sub_mod {α : Type u_1} (l : List α) {i : ℕ} (hi : i < l.length) : (l.rotate i).rotate ((l.length - i) % l.length) = l

Undoing a rotation: (l.rotate i).rotate ((|l| - i) % |l|) = l for i < |l|.

theorem PoissonDeclumping.Lukasiewicz.sub_mod_sub_mod {n i : ℕ} (hi : i < n) : (n - (n - i) % n) % n = i

theorem PoissonDeclumping.PlaneTree.rotate_dfsSeq_mem_bridgeSet (T : PlaneTree) (i : ℕ) : T.dfsSeq.rotate i ∈ Lukasiewicz.bridgeSet T.vertexCount

Every cyclic shift of 𝐱(T) is a bridge sequence of length |T|.

theorem PoissonDeclumping.PlaneTree.finite_vertexCount_eq (n : ℕ) : {T : PlaneTree | T.vertexCount = n}.Finite

There are finitely many plane trees with n vertices.

instance PoissonDeclumping.PlaneTree.instFiniteSubtypeEqNatVertexCount (n : ℕ) : Finite { T : PlaneTree // T.vertexCount = n }

def PoissonDeclumping.PlaneTree.shiftMap (n : ℕ) : { T : PlaneTree // T.vertexCount = n } × Fin n → ↑(Lukasiewicz.bridgeSet n)

The cyclic-shift map (T, i) ↦ 𝐱^{(i)}(T) on trees with n vertices.

Equations

• PoissonDeclumping.PlaneTree.shiftMap n p = ⟨(↑p.1).dfsSeq.rotate ↑p.2, ⋯⟩

@[simp]

theorem PoissonDeclumping.PlaneTree.coe_shiftMap (n : ℕ) (p : { T : PlaneTree // T.vertexCount = n } × Fin n) : ↑(shiftMap n p) = (↑p.1).dfsSeq.rotate ↑p.2

theorem PoissonDeclumping.PlaneTree.shiftMap_bijective (n : ℕ) : Function.Bijective (shiftMap n)

Cyclic shifts and the walk bridge. (T, i) ↦ 𝐱^{(i)}(T) is a bijection from {T : |T| = n} × {0, …, n-1} onto the sequences in ℤ_{≥ -1}^n with sum -1.

noncomputable def PoissonDeclumping.PlaneTree.shiftEquiv (n : ℕ) : { T : PlaneTree // T.vertexCount = n } × Fin n ≃ ↑(Lukasiewicz.bridgeSet n)

The bijection (T, i) ↦ 𝐱^{(i)}(T) behind eq:shifts.

Equations

• PoissonDeclumping.PlaneTree.shiftEquiv n = Equiv.ofBijective (PoissonDeclumping.PlaneTree.shiftMap n) ⋯

@[simp]

theorem PoissonDeclumping.PlaneTree.coe_shiftEquiv_apply (n : ℕ) (p : { T : PlaneTree // T.vertexCount = n } × Fin n) : ↑((shiftEquiv n) p) = (↑p.1).dfsSeq.rotate ↑p.2

theorem PoissonDeclumping.PlaneTree.weight_eq_prod_dfsSeq (μ : PMF ℕ) (T : PlaneTree) : weight μ T = (List.map (fun (a : ℤ) => μ (a + 1).toNat) T.dfsSeq).prod

The Bienaymé weight is the product of the step masses P(X = x) = μ_{x+1} along the DFS sequence.

theorem PoissonDeclumping.PlaneTree.weight_eq_prod_rotate (μ : PMF ℕ) (T : PlaneTree) (i : ℕ) : weight μ T = (List.map (fun (a : ℤ) => μ (a + 1).toNat) (T.dfsSeq.rotate i)).prod

The Bienaymé weight is the product of the step masses along any cyclic shift of the DFS sequence: the weight of (T, i) equals the walk weight of its image 𝐱^{(i)}(T).

theorem PoissonDeclumping.PlaneTree.tsum_sum_weight_mul_rotate (μ : PMF ℕ) (n : ℕ) (g : List ℤ → ENNReal) : ∑' (T : { T : PlaneTree // T.vertexCount = n }), ∑ i : Fin n, weight μ ↑T * g ((↑T).dfsSeq.rotate ↑i) = ∑' (x : ↑(Lukasiewicz.bridgeSet n)), (List.map (fun (a : ℤ) => μ (a + 1).toNat) ↑x).prod * g ↑x

Weighted form of eq:shifts. For every test function g, summing P_μ(T) g(𝐱^{(i)}(T)) over trees with n vertices and shifts i < n gives the sum of P(X_1 = x_1, …, X_n = x_n) g(𝐱) over sequences 𝐱 ∈ ℤ_{≥ -1}^n with sum -1.

theorem PoissonDeclumping.PlaneTree.natCast_mul_tsum_weight_eq (μ : PMF ℕ) (n : ℕ) : (↑n * ∑' (T : PlaneTree), if T.vertexCount = n then weight μ T else 0) = ∑' (x : ↑(Lukasiewicz.bridgeSet n)), (List.map (fun (a : ℤ) => μ (a + 1).toNat) ↑x).prod

Kemperman / Dwass identity (n · P(|𝒯| = n) = P(S_n = -1)), in terms of weights.