Lemma lem:RW: cyclic indicator sums under the walk bridge

Source lines 758–764. For every mark G, every cutoff M ∈ ℕ ∪ {∞} and every n, $$\sum_{i=1}^{n} I^{(M)}_{i}(\mathbf{x}(\mathcal T^{n})) \overset{(d)}{=} \sum_{i=1}^{n} I^{(M)}_{i}(X_{1}, \ldots,X_{n}) \text{ under } P(\cdot \mid S_{n}=-1).$$

Cyclic.map_cyclicSum_conditioned states this as an equality of laws on ℕ: the push-forward of 𝒯^n = PlaneTree.conditioned μ n under T ↦ ∑_i I_i^{(M)}(𝐱(T)) equals the push-forward of Lukasiewicz.bridgeLaw μ n (the law of (X_1, …, X_n) given S_n = -1) under ω ↦ ∑_i I_i^{(M)}(ω). It holds for every n: at inadmissible n both sides are the zero measure (Cyclic.bridgeLaw_eq_zero_of_not_admissible).

The proof is the paper's: eq:shifts (PlaneTree.map_shift_conditioned) and the invariance of the cyclic sum under cyclic shifts (Cyclic.cyclicSum_rotate, B04). Combined with the counting identity, the law of the (truncated) number of marked fringe subtrees of 𝒯^n is the law of the cyclic sum under the bridge (Cyclic.map_markCount_conditioned, Cyclic.markedCountLaw_eq).

B04, second part: the bridge law is invariant under permutations of the coordinates (Cyclic.map_bridgeLaw_comp_perm), so all cyclic indicators have the same law under the bridge (Cyclic.bridgeLaw_shiftIndicator_eq_one) and E[∑_i I_i^{(M)} | S_n = -1] = n P(I_1^{(M)} = 1 | S_n = -1) (Cyclic.lintegral_cyclicSum_bridgeLaw).

theorem PoissonDeclumping.Cyclic.uniformIndex_univ {n : ℕ} (hn : n ≠ 0) : (PlaneTree.uniformIndex n) Set.univ = 1

The uniform index law has total mass one for n ≠ 0.

theorem PoissonDeclumping.Cyclic.bridgeLaw_eq_zero_of_not_admissible (μ : PMF ℕ) {n : ℕ} (h : ¬PlaneTree.Admissible μ n) : Lukasiewicz.bridgeLaw μ n = 0

(X_1, …, X_n) given S_n = -1 is the zero measure when S_n = -1 is impossible.

theorem PoissonDeclumping.Cyclic.ae_vertexCount_prod (μ : PMF ℕ) (n : ℕ) : ∀ᵐ (p : PlaneTree × Fin n) ∂(PlaneTree.conditioned μ n).prod (PlaneTree.uniformIndex n), p.1.vertexCount = n

Under 𝒯^n ⊗ Unif{0, …, n-1}, the tree has n vertices almost surely.

theorem PoissonDeclumping.Cyclic.map_cyclicSum_conditioned (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ∞) (n : ℕ) : MeasureTheory.Measure.map (fun (T : PlaneTree) => cyclicSum G M T.dfsSeq) (PlaneTree.conditioned μ n) = MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => cyclicSum G M (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n)

Lemma lem:RW. For every mark G, cutoff M ∈ ℕ ∪ {∞} and size n, the law of ∑_{i=1}^{n} I_i^{(M)}(𝐱(𝒯^n)) equals the law of ∑_{i=1}^{n} I_i^{(M)}(X_1, …, X_n) under P(· | S_n = -1).

theorem PoissonDeclumping.Cyclic.map_markCount_conditioned (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ∞) (n : ℕ) : MeasureTheory.Measure.map (PlaneTree.markCount fun (U : PlaneTree) => ↑U.vertexCount ≤ M ∧ G U) (PlaneTree.conditioned μ n) = MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => cyclicSum G M (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n)

Lemma lem:RW, count form. The law of the number of vertices v of 𝒯^n with |𝒯^n_v| ≤ M and G(𝒯^n_v) = 1 (the truncated count when M < n) is the law of ∑_{i=1}^{n} I_i^{(M)}(X_1, …, X_n) under P(· | S_n = -1).

theorem PoissonDeclumping.Cyclic.map_markCount_conditioned_of_le (μ : PMF ℕ) (G : PlaneTree → Prop) {M : ℕ∞} {n : ℕ} (hM : ↑n ≤ M) : MeasureTheory.Measure.map (PlaneTree.markCount G) (PlaneTree.conditioned μ n) = MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => cyclicSum G M (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n)

Lemma lem:RW, untruncated count. For M ≥ n (e.g. M = ∞), the law of the number #{u ∈ 𝒯^n : G(𝒯^n_u) = 1} of marked vertices of 𝒯^n is the law of ∑_{i=1}^{n} I_i^{(M)}(X_1, …, X_n) under P(· | S_n = -1).

theorem PoissonDeclumping.Cyclic.markedCountLaw_eq (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) (n : ℕ) : markedCountLaw μ G k n = MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => cyclicSum (G (k n)) ⊤ (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n)

The law markedCountLaw μ G k n of #{u ∈ 𝒯^n : G_{k_n}(𝒯^n_u) = 1} (Setup/Marks.lean) is the law of ∑_{i=1}^{n} I_i^{(∞)}(X_1, …, X_n) under P(· | S_n = -1).

Exchangeability of the cyclic indicators under the bridge (B04)

theorem PoissonDeclumping.Cyclic.ofFn_comp_finRotate {α : Type u_1} {n : ℕ} (f : Fin n → α) : List.ofFn (f ∘ ⇑(finRotate n)) = (List.ofFn f).rotate 1

Rotating the coordinates by one step rotates the list by one.

theorem PoissonDeclumping.Cyclic.ofFn_comp_finRotate_pow {α : Type u_1} {n : ℕ} (f : Fin n → α) (i : ℕ) : List.ofFn (f ∘ ⇑(finRotate n ^ i)) = (List.ofFn f).rotate i

theorem PoissonDeclumping.Cyclic.map_walkVecLaw_comp_perm (μ : PMF ℕ) {n : ℕ} (σ : Equiv.Perm (Fin n)) : MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => ω ∘ ⇑σ) (Lukasiewicz.walkVecLaw μ n) = Lukasiewicz.walkVecLaw μ n

The law of (X_1, …, X_n) is invariant under permutations of the coordinates.

theorem PoissonDeclumping.Cyclic.map_bridgeLaw_comp_perm (μ : PMF ℕ) {n : ℕ} (σ : Equiv.Perm (Fin n)) : MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => ω ∘ ⇑σ) (Lukasiewicz.bridgeLaw μ n) = Lukasiewicz.bridgeLaw μ n

The bridge law is invariant under permutations of the coordinates.

theorem PoissonDeclumping.Cyclic.bridgeLaw_shiftIndicator_eq_one (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ∞) (n i : ℕ) : (Lukasiewicz.bridgeLaw μ n) {ω : Fin n → ℤ | shiftIndicator G M (List.ofFn ω) i = 1} = (Lukasiewicz.bridgeLaw μ n) {ω : Fin n → ℤ | firstIndicator G M (List.ofFn ω) = 1}

B04, second part. Under the bridge P(· | S_n = -1), all cyclic indicators have the same law: P(I_{i+1}^{(M)}(X_1, …, X_n) = 1 | S_n = -1) = P(I_1^{(M)}(X_1, …, X_n) = 1 | S_n = -1).

theorem PoissonDeclumping.Cyclic.lintegral_cyclicSum_bridgeLaw (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ∞) (n : ℕ) : ∫⁻ (ω : Fin n → ℤ), ↑(cyclicSum G M (List.ofFn ω)) ∂Lukasiewicz.bridgeLaw μ n = ↑n * (Lukasiewicz.bridgeLaw μ n) {ω : Fin n → ℤ | firstIndicator G M (List.ofFn ω) = 1}

Consequently E[∑_{i=1}^n I_i^{(M)}(X_1, …, X_n) | S_n = -1] = n P(I_1^{(M)} = 1 | S_n = -1).