The DFS law of 𝒯^n and the cyclic-shift law eq:shifts

Section 2.2 of the paper (source lines 718–730), as equalities of measures.

Let 𝐗 = (X_i)_{i ≥ 1} be i.i.d. with P(X_1 = i) = μ_{i+1} for i ≥ -1 (Lukasiewicz.stepPMF μ), and S_k = X_1 + ⋯ + X_k. The law of (X_1, …, X_n) is the product measure Lukasiewicz.walkVecLaw μ n on Fin n → ℤ.

• PlaneTree.map_dfsSeq_conditioned: the DFS sequence of 𝒯^n has the law of (X_1, …, X_n) under P(· | ζ(𝐗) = n).
• PlaneTree.map_shift_conditioned (eq:shifts): if I is uniform on {0, …, n-1} and independent of 𝒯^n, then the I-th cyclic shift 𝐱^{(I)}(𝒯^n) has the law of (X_1, …, X_n) under P(· | S_n = -1).
• PlaneTree.walkVecLaw_sum_eq_neg_one: P(S_n = -1) = n P(|𝒯| = n) (Kemperman / Dwass).

Here 𝒯^n is PlaneTree.conditioned μ n, the μ-Bienaymé weights conditioned on |T| = n. None of these statements needs criticality or normalization of the tree law: the conditioned weights are normalized by their own total mass, and both sides are the zero measure when P(|𝒯| = n) = 0. The paper's sequences are indexed from 1; ours from 0.

noncomputable def PoissonDeclumping.Lukasiewicz.stepPMF (μ : PMF ℕ) : PMF ℤ

The step law P(X = i) = μ_{i+1} (i ≥ -1): the image of μ under k ↦ k - 1.

Equations

• PoissonDeclumping.Lukasiewicz.stepPMF μ = PMF.map (fun (k : ℕ) => ↑k - 1) μ

theorem PoissonDeclumping.Lukasiewicz.stepPMF_apply (μ : PMF ℕ) (a : ℤ) : (stepPMF μ) a = if -1 ≤ a then μ (a + 1).toNat else 0

noncomputable def PoissonDeclumping.Lukasiewicz.walkVecLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure (Fin n → ℤ)

The law of (X_1, …, X_n): n independent steps with law stepPMF μ.

Equations

• PoissonDeclumping.Lukasiewicz.walkVecLaw μ n = MeasureTheory.Measure.pi fun (x : Fin n) => (PoissonDeclumping.Lukasiewicz.stepPMF μ).toMeasure

instance PoissonDeclumping.Lukasiewicz.instIsProbabilityMeasureForallFinIntWalkVecLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (walkVecLaw μ n)

theorem PoissonDeclumping.Lukasiewicz.walkVecLaw_singleton (μ : PMF ℕ) (n : ℕ) (ω : Fin n → ℤ) : (walkVecLaw μ n) {ω} = ∏ i : Fin n, (stepPMF μ) (ω i)

noncomputable def PoissonDeclumping.Lukasiewicz.bridgeLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure (Fin n → ℤ)

(X_1, …, X_n) under P(· | S_n = -1).

Equations

• PoissonDeclumping.Lukasiewicz.bridgeLaw μ n = (PoissonDeclumping.Lukasiewicz.walkVecLaw μ n)[|{ω : Fin n → ℤ | ∑ i : Fin n, ω i = -1}]

noncomputable def PoissonDeclumping.Lukasiewicz.excursionLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure (Fin n → ℤ)

(X_1, …, X_n) under P(· | ζ(𝐗) = n).

Equations

• PoissonDeclumping.Lukasiewicz.excursionLaw μ n = (PoissonDeclumping.Lukasiewicz.walkVecLaw μ n)[|{ω : Fin n → ℤ | PoissonDeclumping.Lukasiewicz.zeta (List.ofFn ω) = some n}]

def PoissonDeclumping.Lukasiewicz.toVec (n : ℕ) (x : List ℤ) : Fin n → ℤ

A list read as a vector of length n (padded by zeros, truncated after n entries).

Equations

• PoissonDeclumping.Lukasiewicz.toVec n x k = x.getD (↑k) 0

theorem PoissonDeclumping.Lukasiewicz.toVec_ofFn {n : ℕ} (ω : Fin n → ℤ) : toVec n (List.ofFn ω) = ω

theorem PoissonDeclumping.Lukasiewicz.ofFn_toVec {n : ℕ} {x : List ℤ} (hx : x.length = n) : List.ofFn (toVec n x) = x

theorem PoissonDeclumping.Lukasiewicz.walkWeight_ofFn (μ : PMF ℕ) {n : ℕ} (ω : Fin n → ℤ) (hω : ∀ (i : Fin n), -1 ≤ ω i) : walkWeight μ (List.ofFn ω) = ∏ i : Fin n, (stepPMF μ) (ω i)

theorem PoissonDeclumping.Lukasiewicz.tsum_walkWeight_mul_toVec {n : ℕ} (μ : PMF ℕ) {A : Set (List ℤ)} (hA : ∀ x ∈ A, x.length = n ∧ ∀ a ∈ x, -1 ≤ a) (ω : Fin n → ℤ) : (∑' (x : ↑A), walkWeight μ ↑x * if toVec n ↑x = ω then 1 else 0) = if List.ofFn ω ∈ A then ∏ i : Fin n, (stepPMF μ) (ω i) else 0

Point masses of the walk law against a set A of admissible lists.

theorem PoissonDeclumping.Lukasiewicz.walkVecLaw_inter_singleton {n : ℕ} (μ : PMF ℕ) {A : Set (List ℤ)} {B : Set (Fin n → ℤ)} (hA : ∀ x ∈ A, x.length = n ∧ ∀ a ∈ x, -1 ≤ a) (hAB : ∀ (ω : Fin n → ℤ), List.ofFn ω ∈ A ↔ ω ∈ B ∧ ∀ (i : Fin n), -1 ≤ ω i) (ω : Fin n → ℤ) : (walkVecLaw μ n) (B ∩ {ω}) = ∑' (x : ↑A), walkWeight μ ↑x * if toVec n ↑x = ω then 1 else 0

The walk law of B ∩ {ω}, when B corresponds to a set A of admissible lists.

theorem PoissonDeclumping.Lukasiewicz.walkVecLaw_eq_tsum {n : ℕ} (μ : PMF ℕ) {A : Set (List ℤ)} {B : Set (Fin n → ℤ)} (hA : ∀ x ∈ A, x.length = n ∧ ∀ a ∈ x, -1 ≤ a) (hAB : ∀ (ω : Fin n → ℤ), List.ofFn ω ∈ A ↔ ω ∈ B ∧ ∀ (i : Fin n), -1 ≤ ω i) : (walkVecLaw μ n) B = ∑' (x : ↑A), walkWeight μ ↑x

The walk law of B, when B corresponds to a set A of admissible lists.

theorem PoissonDeclumping.Lukasiewicz.bridgeSet_admissible (n : ℕ) (x : List ℤ) : x ∈ bridgeSet n → x.length = n ∧ ∀ a ∈ x, -1 ≤ a

theorem PoissonDeclumping.Lukasiewicz.ofFn_mem_bridgeSet_iff {n : ℕ} (ω : Fin n → ℤ) : List.ofFn ω ∈ bridgeSet n ↔ ω ∈ {ω : Fin n → ℤ | ∑ i : Fin n, ω i = -1} ∧ ∀ (i : Fin n), -1 ≤ ω i

theorem PoissonDeclumping.Lukasiewicz.excursionSet_admissible (n : ℕ) (x : List ℤ) : x ∈ excursionSet n → x.length = n ∧ ∀ a ∈ x, -1 ≤ a

theorem PoissonDeclumping.Lukasiewicz.ofFn_mem_excursionSet_iff {n : ℕ} (ω : Fin n → ℤ) : List.ofFn ω ∈ excursionSet n ↔ ω ∈ {ω : Fin n → ℤ | zeta (List.ofFn ω) = some n} ∧ ∀ (i : Fin n), -1 ≤ ω i

theorem PoissonDeclumping.Lukasiewicz.walkVecLaw_sum_eq_neg_one_eq_walkMass (μ : PMF ℕ) (n : ℕ) : (walkVecLaw μ n) {ω : Fin n → ℤ | ∑ i : Fin n, ω i = -1} = walkMass μ n (-1)

P(S_n = -1) = Ψ_n(-1).

theorem PoissonDeclumping.Lukasiewicz.walkVecLaw_zeta_eq (μ : PMF ℕ) (n : ℕ) : (walkVecLaw μ n) {ω : Fin n → ℤ | zeta (List.ofFn ω) = some n} = ∑' (x : ↑(excursionSet n)), walkWeight μ ↑x

P(ζ(𝐗) = n) is the total walk weight of {ζ = n}.

theorem PoissonDeclumping.PlaneTree.conditioned_singleton (μ : PMF ℕ) (n : ℕ) (T : PlaneTree) : (conditioned μ n) {T} = ((bienayme μ) {T : PlaneTree | T.vertexCount = n})⁻¹ * if T.vertexCount = n then weight μ T else 0

instance PoissonDeclumping.PlaneTree.instIsZeroOrProbabilityMeasureConditioned (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsZeroOrProbabilityMeasure (conditioned μ n)

theorem PoissonDeclumping.PlaneTree.walkVecLaw_sum_eq_neg_one (μ : PMF ℕ) (n : ℕ) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | ∑ i : Fin n, ω i = -1} = ↑n * (bienayme μ) {T : PlaneTree | T.vertexCount = n}

Kemperman / Dwass identity: P(S_n = -1) = n P(|𝒯| = n).

theorem PoissonDeclumping.PlaneTree.walkVecLaw_zeta_eq_bienayme (μ : PMF ℕ) (n : ℕ) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | Lukasiewicz.zeta (List.ofFn ω) = some n} = (bienayme μ) {T : PlaneTree | T.vertexCount = n}

P(ζ(𝐗) = n) = P(|𝒯| = n).

theorem PoissonDeclumping.PlaneTree.tsum_sum_weight_mul_rotate_walkWeight (μ : 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)), Lukasiewicz.walkWeight μ ↑x * g ↑x

tsum_sum_weight_mul_rotate, with the step weights written as walkWeight.

theorem PoissonDeclumping.PlaneTree.tsum_conditioned_singleton_mul (μ : PMF ℕ) (n : ℕ) (h : PlaneTree → ENNReal) : ∑' (T : PlaneTree), (conditioned μ n) {T} * h T = ((bienayme μ) {T : PlaneTree | T.vertexCount = n})⁻¹ * ∑' (T : { T : PlaneTree // T.vertexCount = n }), weight μ ↑T * h ↑T

Sums against the conditioned law, in weights.

theorem PoissonDeclumping.PlaneTree.map_dfsSeq_conditioned (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure.map (fun (T : PlaneTree) => Lukasiewicz.toVec n T.dfsSeq) (conditioned μ n) = Lukasiewicz.excursionLaw μ n

DFS law of 𝒯^n. The DFS sequence of 𝒯^n has the law of (X_1, …, X_n) under P(· | ζ(𝐗) = n).

noncomputable def PoissonDeclumping.PlaneTree.uniformIndex (n : ℕ) : MeasureTheory.Measure (Fin n)

The uniform law on {0, …, n-1}.

Equations

• PoissonDeclumping.PlaneTree.uniformIndex n = MeasureTheory.Measure.uniformOfFinset Finset.univ

theorem PoissonDeclumping.PlaneTree.uniformIndex_singleton (n : ℕ) (i : Fin n) : (uniformIndex n) {i} = (↑n)⁻¹

theorem PoissonDeclumping.PlaneTree.map_shift_conditioned (μ : PMF ℕ) {n : ℕ} (hn : n ≠ 0) : MeasureTheory.Measure.map (fun (p : PlaneTree × Fin n) => Lukasiewicz.toVec n (p.1.dfsSeq.rotate ↑p.2)) ((conditioned μ n).prod (uniformIndex n)) = Lukasiewicz.bridgeLaw μ n

eq:shifts. If I is uniform on {0, …, n-1} and independent of 𝒯^n, then the cyclic shift 𝐱^{(I)}(𝒯^n) has the law of (X_1, …, X_n) under P(· | S_n = -1).