Corollary cor:cyclicshift: the fringe subtree at a uniform vertex

Source lines 777–825 (Corollary 2.3 and its proof), 227–229 (U01, first part) and 914–920, 960–969 (U05).

Let U_n be a uniform vertex of 𝒯^n, independent of 𝒯^n; the law of 𝒯^n_{U_n} is uniformFringeLaw μ n (Setup/Marks.lean). We prove, following the paper's proof:

• Cyclic.bridgeLaw_ofSeq_mem (first step of the proof): the tree T(X_1, …, X_n) encoded by the bridge (X_1, …, X_n) under P(· | S_n = -1) has the law of 𝒯^n_{U_n}; in indicator form P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| ≤ M) = P(I_1^{(M)}(X_1, …, X_n) = 1 | S_n = -1) (Cyclic.uniformFringeLaw_truncated_eq_bridgeLaw), and for M = n the paper's P(G(𝒯^n_{U_n}) = 1) = P(I_1^{(n)} = 1 | S_n = -1) (Cyclic.uniformFringeLaw_eq_bridgeLaw);
• Cyclic.walkVecLaw_bridge_inter_ofSeq (Markov property at ζ, P01): P(T(𝐗) ∈ s, S_n = -1) = E[1_{𝒯 ∈ s} Ψ_{n-|𝒯|}(0)] (the remainder endpoint is 0), and the paper's form ∑_{m ≥ 1} P(𝒯 ∈ s, |𝒯| = m) Ψ_{n-m}(0) (Cyclic.walkVecLaw_bridge_inter_ofSeq_eq_tsum);
• Corollary cor:cyclicshift in ℝ≥0∞ (Cyclic.uniformFringeLaw_eq) and in ℝ exactly as stated (Cyclic.uniformFringeLaw_real_eq): P(G(𝒯^n_{U_n}) = 1) = Ψ_n(-1)⁻¹ E[1_{G(𝒯) = 1} Ψ_{n-|𝒯|}(0)], with Ψ_m = 0 for m < 0 built into walkProb; and the truncated version (Cyclic.uniformFringeLaw_real_truncated);
• U01, first part: E[#{u ∈ 𝒯^n : G(𝒯^n_u) = 1}] = n P(G(𝒯^n_{U_n}) = 1) (Cyclic.lintegral_markCount_conditioned, Cyclic.integral_markCount_conditioned);
• U05: if the mark G_{k_n} forces the size k_n, then A_n(ℓ) = 0 for every ℓ ≥ 1 (Cyclic.pairProb_eq_zero_of_forces_size).

All identities hold for every n. The paper restricts to admissible n; at an inadmissible n both sides vanish (𝒯^n is then the zero measure, Ψ_n(-1) = 0, and 0⁻¹ = 0 in ℝ). The expectation E is the integral against PlaneTree.bienayme μ; no criticality is needed.

The law of 𝒯^n_{U_n}

theorem PoissonDeclumping.Cyclic.uniformOn_Iio_eq_map (n : ℕ) : ProbabilityTheory.uniformOn (Set.Iio n) = MeasureTheory.Measure.map Fin.val (PlaneTree.uniformIndex n)

The uniform law on {0, …, n-1} ⊆ ℕ is the image of the uniform law on Fin n.

theorem PoissonDeclumping.Cyclic.uniformFringeLaw_eq_map (μ : PMF ℕ) (n : ℕ) : uniformFringeLaw μ n = MeasureTheory.Measure.map (fun (p : PlaneTree × Fin n) => p.1.fringeTrees.getD (↑p.2) p.1) ((PlaneTree.conditioned μ n).prod (PlaneTree.uniformIndex n))

The law of 𝒯^n_{U_n} is the image of 𝒯^n ⊗ Unif(Fin n) under (T, i) ↦ T_{u_i}.

theorem PoissonDeclumping.Cyclic.isProbabilityMeasure_uniformFringeLaw {μ : PMF ℕ} {n : ℕ} (h : PlaneTree.Admissible μ n) : MeasureTheory.IsProbabilityMeasure (uniformFringeLaw μ n)

At an admissible size, the law of 𝒯^n_{U_n} is a probability measure.

theorem PoissonDeclumping.Cyclic.bridgeLaw_ofSeq_mem (μ : PMF ℕ) (n : ℕ) (s : Set PlaneTree) : (Lukasiewicz.bridgeLaw μ n) {ω : Fin n → ℤ | ∃ T ∈ s, PlaneTree.ofSeq (List.ofFn ω) = some T} = (uniformFringeLaw μ n) s

First step of the proof of cor:cyclicshift. The tree T(X_1, …, X_n) encoded by the first excursion of (X_1, …, X_n) under P(· | S_n = -1) has the law of 𝒯^n_{U_n}.

theorem PoissonDeclumping.Cyclic.uniformFringeLaw_truncated_eq_bridgeLaw (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → Prop) (M : ℕ∞) : (uniformFringeLaw μ n) {T : PlaneTree | ↑T.vertexCount ≤ M ∧ G T} = (Lukasiewicz.bridgeLaw μ n) {ω : Fin n → ℤ | firstIndicator G M (List.ofFn ω) = 1}

P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| ≤ M) = P(I_1^{(M)}(X_1, …, X_n) = 1 | S_n = -1).

theorem PoissonDeclumping.Cyclic.uniformFringeLaw_vertexCount_gt (μ : PMF ℕ) (n : ℕ) : (uniformFringeLaw μ n) {T : PlaneTree | n < T.vertexCount} = 0

The fringe subtree at a uniform vertex of 𝒯^n has at most n vertices almost surely.

theorem PoissonDeclumping.Cyclic.uniformFringeLaw_eq_bridgeLaw (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → Prop) : (uniformFringeLaw μ n) {T : PlaneTree | G T} = (Lukasiewicz.bridgeLaw μ n) {ω : Fin n → ℤ | firstIndicator G (↑n) (List.ofFn ω) = 1}

First display of the proof of cor:cyclicshift: P(G(𝒯^n_{U_n}) = 1) = P(I_1^{(n)}(X_1, …, X_n) = 1 | S_n = -1).

The Markov property at ζ on the bridge (P01)

theorem PoissonDeclumping.Cyclic.lintegral_indicator_vertexCount (μ : PMF ℕ) (s : Set PlaneTree) (g : ℕ → ENNReal) : ∫⁻ (T : PlaneTree), s.indicator (fun (T : PlaneTree) => g T.vertexCount) T ∂PlaneTree.bienayme μ = ∑' (m : ℕ), (PlaneTree.bienayme μ) (s ∩ {T : PlaneTree | T.vertexCount = m}) * g m

∫⁻ 1_{𝒯 ∈ s} g(|𝒯|) dP_μ = ∑_m P_μ(𝒯 ∈ s, |𝒯| = m) g(m).

theorem PoissonDeclumping.Cyclic.walkVecLaw_bridge_inter_ofSeq (μ : PMF ℕ) (n : ℕ) (s : Set PlaneTree) : (Lukasiewicz.walkVecLaw μ n) ({ω : Fin n → ℤ | ∑ i : Fin n, ω i = -1} ∩ {ω : Fin n → ℤ | ∃ T ∈ s, PlaneTree.ofSeq (List.ofFn ω) = some T}) = ∫⁻ (T : PlaneTree), s.indicator (fun (T : PlaneTree) => if T.vertexCount ≤ n then (walkLaw μ (n - T.vertexCount)) {0} else 0) T ∂PlaneTree.bienayme μ

Markov property at ζ (P01). P(T(X_1, …, X_n) ∈ s, S_n = -1) = E[1_{𝒯 ∈ s} Ψ_{n-|𝒯|}(0)], with Ψ_{n-m}(0) = 0 for m > n: after the first excursion (ending at level -1 at time ζ), the walk must return from -1 to -1, i.e. make a fresh walk of length n - ζ ending at 0.

theorem PoissonDeclumping.Cyclic.walkVecLaw_bridge_inter_ofSeq_eq_tsum (μ : PMF ℕ) (n : ℕ) (s : Set PlaneTree) : (Lukasiewicz.walkVecLaw μ n) ({ω : Fin n → ℤ | ∑ i : Fin n, ω i = -1} ∩ {ω : Fin n → ℤ | ∃ T ∈ s, PlaneTree.ofSeq (List.ofFn ω) = some T}) = ∑' (m : ℕ), (PlaneTree.bienayme μ) (s ∩ {T : PlaneTree | T.vertexCount = m}) * if m ≤ n then (walkLaw μ (n - m)) {0} else 0

Markov property at ζ, the paper's form: P(T(𝐗) ∈ s, S_n = -1) = ∑_{m ≥ 1} P(𝒯 ∈ s, |𝒯| = m) Ψ_{n-m}(0), with Ψ_{n-m}(0) = 0 for m > n (and the m = 0 term vanishes since no tree has 0 vertices).

Corollary cor:cyclicshift

theorem PoissonDeclumping.Cyclic.uniformFringeLaw_eq (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → Prop) : (uniformFringeLaw μ n) {T : PlaneTree | G T} = ((walkLaw μ n) {-1})⁻¹ * ∫⁻ (T : PlaneTree), {T : PlaneTree | G T}.indicator (fun (T : PlaneTree) => if T.vertexCount ≤ n then (walkLaw μ (n - T.vertexCount)) {0} else 0) T ∂PlaneTree.bienayme μ

Corollary cor:cyclicshift in ℝ≥0∞: P(G(𝒯^n_{U_n}) = 1) = Ψ_n(-1)⁻¹ E[1_{G(𝒯) = 1} Ψ_{n-|𝒯|}(0)], where Ψ_n(-1) = P(S_n = -1) and Ψ_{n-m}(0) = P(S_{n-m} = 0) for m ≤ n, 0 for m > n.

theorem PoissonDeclumping.Cyclic.uniformFringeLaw_real_eq (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → Prop) : (uniformFringeLaw μ n).real {T : PlaneTree | G T} = (walkProb μ (↑n) (-1))⁻¹ * ∫ (T : PlaneTree), {T : PlaneTree | G T}.indicator (fun (T : PlaneTree) => walkProb μ (↑n - ↑T.vertexCount) 0) T ∂PlaneTree.bienayme μ

Corollary cor:cyclicshift, exactly as stated, in ℝ: P(G(𝒯^n_{U_n}) = 1) = (1 / Ψ_n(-1)) E[1_{G(𝒯) = 1} Ψ_{n-|𝒯|}(0)], with U_n a uniform vertex of 𝒯^n independent of 𝒯^n, 𝒯 a μ-Bienaymé tree, Ψ_m(i) = P(S_m = i) and Ψ_m(i) = 0 for m < 0.

theorem PoissonDeclumping.Cyclic.uniformFringeLaw_real_truncated (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → Prop) (M : ℕ∞) : (Lukasiewicz.bridgeLaw μ n).real {ω : Fin n → ℤ | firstIndicator G M (List.ofFn ω) = 1} = (uniformFringeLaw μ n).real {T : PlaneTree | ↑T.vertexCount ≤ M ∧ G T} ∧ (uniformFringeLaw μ n).real {T : PlaneTree | ↑T.vertexCount ≤ M ∧ G T} = (walkProb μ (↑n) (-1))⁻¹ * ∫ (T : PlaneTree), {T : PlaneTree | ↑T.vertexCount ≤ M ∧ G T}.indicator (fun (T : PlaneTree) => walkProb μ (↑n - ↑T.vertexCount) 0) T ∂PlaneTree.bienayme μ

Corollary cor:cyclicshift, truncated version: P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| ≤ M) = P(I_1^{(M)}(X_1, …, X_n) = 1 | S_n = -1) = (1 / Ψ_n(-1)) E[1_{G(𝒯) = 1, |𝒯| ≤ M} Ψ_{n-|𝒯|}(0)].

theorem PoissonDeclumping.Cyclic.uniformFringeLaw_real_eq_bridgeLaw (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → Prop) : (uniformFringeLaw μ n).real {T : PlaneTree | G T} = (Lukasiewicz.bridgeLaw μ n).real {ω : Fin n → ℤ | firstIndicator G (↑n) (List.ofFn ω) = 1}

Corollary cor:cyclicshift, bridge form: P(G(𝒯^n_{U_n}) = 1) = P(I_1^{(n)}(X_1, …, X_n) = 1 | S_n = -1), in ℝ.

U01, first part: expected count and uniform vertex

theorem PoissonDeclumping.Cyclic.markCount_eq_card (G : PlaneTree → Prop) (T : PlaneTree) [DecidablePred G] : PlaneTree.markCount G T = {i : Fin T.vertexCount | G (T.fringeTrees.getD (↑i) T)}.card

markCount G T as the number of DFS indices i < |T| whose fringe tree is marked.

theorem PoissonDeclumping.Cyclic.lintegral_markCount_conditioned (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → Prop) : ∫⁻ (T : PlaneTree), ↑(PlaneTree.markCount G T) ∂PlaneTree.conditioned μ n = ↑n * (uniformFringeLaw μ n) {T : PlaneTree | G T}

U01, first part (source lines 227–229). E[#{u ∈ 𝒯^n : G(𝒯^n_u) = 1}] = n P(G(𝒯^n_{U_n}) = 1), in ℝ≥0∞.

theorem PoissonDeclumping.Cyclic.integral_markCount_conditioned (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → Prop) : ∫ (T : PlaneTree), ↑(PlaneTree.markCount G T) ∂PlaneTree.conditioned μ n = ↑n * (uniformFringeLaw μ n).real {T : PlaneTree | G T}

U01, first part, in ℝ: E[#{u ∈ 𝒯^n : G(𝒯^n_u) = 1}] = n P(G(𝒯^n_{U_n}) = 1).

U05: marks forcing the size exclude nested pairs

theorem PoissonDeclumping.Cyclic.pairProb_eq_zero_of_forces_size (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) (n : ℕ) (hG : ∀ (τ : PlaneTree), G (k n) τ → τ.vertexCount = k n) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) : pairProb μ G k n ℓ = 0

U05. If the mark G_{k_n} forces the size k_n (G_{k_n}(τ) = 1 ⇒ |τ| = k_n), then A_n(ℓ) = 0 for every ℓ ≥ 1: a fringe subtree cannot contain a proper fringe subtree of the same size.