The two-start bound (P11, Lemma lem:boundb2)

Work package WP4.7 of the bridge plan (no toolkit). Source lines 1832–1845.

The paper bounds E[I_1^{(M_n)} I_{1+ℓ}^{(M_n)}] (unconditioned walk) by π_n² + A_n(ℓ). Its argument says that if v_{1+ℓ} is not in the first tree 𝒯, then the occurrences at v_1 and v_{1+ℓ} lie in "two independent Bienaymé trees"; the event {v_{1+ℓ} ∉ 𝒯} = {|𝒯| ≤ ℓ} depends on 𝒯, so this is made precise here (audit finding 5) by conditioning on the first passage time ζ = j: for j ≤ ℓ the indicator at ℓ + 1 is a function of the fresh increments after ζ (walkVecLaw_zeta_eq_inter_drop), and for j > ℓ the vertex v_{1+ℓ} is u_{ℓ+1}(𝒯).

Main statements

• walkVecLaw_ofSeq_mem_le: P(T(X_1..X_N) ∈ A) ≤ P(𝒯 ∈ A).
• walkVecLaw_firstMarked_pair_le (measure form, non-cyclic indicator): P(I_1^{(M)} = 1, I_1^{(M)}(X_{ℓ+1}, …) = 1) ≤ P(G(𝒯)) P(G(𝒯), |𝒯| ≤ M) + A(ℓ) for ℓ + M ≤ N.
• walkVecLaw_real_firstMarked_pair_le: the same in ℝ with the cyclic indicator I_{1+ℓ}^{(M)}, bounded by P(G(𝒯))² + A(ℓ); walkVecLaw_real_pair_le_markProb: the paper's form ≤ π_n² + A_n(ℓ) with markProb and pairProb of Setup/Marks.lean.

No restriction ℓ ≥ 1 is needed (for ℓ = 0 the bound is trivial).

theorem PoissonDeclumping.Bridge.walkVecLaw_ofSeq_mem_le (μ : PMF ℕ) (N : ℕ) (A : Set PlaneTree) : (Lukasiewicz.walkVecLaw μ N) {ω : Fin N → ℤ | ∃ T ∈ A, PlaneTree.ofSeq (List.ofFn ω) = some T} ≤ (PlaneTree.bienayme μ) A

P(T(X_1, …, X_N) ∈ A) ≤ P(𝒯 ∈ A): the first tree encoded by the walk is a Bienaymé tree (cut at size N).

theorem PoissonDeclumping.Bridge.sum_bienayme_vertexCount_eq_le (μ : PMF ℕ) (J : Finset ℕ) (A : Set PlaneTree) : ∑ j ∈ J, (PlaneTree.bienayme μ) (A ∩ {T : PlaneTree | T.vertexCount = j}) ≤ (PlaneTree.bienayme μ) A

∑_{j ∈ J} P(𝒯 ∈ A, |𝒯| = j) ≤ P(𝒯 ∈ A).

theorem PoissonDeclumping.Bridge.walkVecLaw_firstMarked_pair_le (μ : PMF ℕ) (G : PlaneTree → Prop) {M N ℓ : ℕ} (hN : ℓ + M ≤ N) : (Lukasiewicz.walkVecLaw μ N) {ω : Fin N → ℤ | Cyclic.FirstMarked G (↑M) (List.ofFn ω) ∧ Cyclic.FirstMarked G (↑M) (List.drop ℓ (List.ofFn ω))} ≤ (PlaneTree.bienayme μ) {T : PlaneTree | G T} * (PlaneTree.bienayme μ) {T : PlaneTree | G T ∧ T.vertexCount ≤ M} + (PlaneTree.bienayme μ) {T : PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ G T ∧ ∃ U ∈ T.fringeTrees[ℓ]?, G U}

Two-start bound (P11, Lemma lem:boundb2, source lines 1832–1845, corrected as in audit finding 5). Let ℓ + M ≤ N. Then P(I_1^{(M)} = 1, I_{1+ℓ}^{(M)} = 1) ≤ P(G(𝒯) = 1) P(G(𝒯) = 1, |𝒯| ≤ M) + P(|𝒯| ≥ ℓ + 1, G(𝒯) = 1, G(𝒯_{u_{ℓ+1}}) = 1), where I_{1+ℓ}^{(M)} reads X_{ℓ+1}, …, X_{ℓ+M}.

The proof conditions on the first passage time ζ = j: if j ≤ ℓ, the indicator at ℓ + 1 only depends on the fresh increments after ζ (strong Markov property at ζ); if j > ℓ, the vertex v_{ℓ+1} lies in the first tree 𝒯 = T(𝐗) and I_{1+ℓ}^{(M)} = 1 forces G(𝒯_{u_{ℓ+1}}) = 1.

theorem PoissonDeclumping.Bridge.walkVecLaw_real_firstMarked_pair_le (μ : PMF ℕ) (G : PlaneTree → Prop) {M N ℓ : ℕ} (hN : ℓ + M ≤ N) : (Lukasiewicz.walkVecLaw μ N).real {ω : Fin N → ℤ | Cyclic.FirstMarked G (↑M) (List.ofFn ω) ∧ Cyclic.FirstMarked G (↑M) ((List.ofFn ω).rotate ℓ)} ≤ (PlaneTree.bienayme μ).real {T : PlaneTree | G T} ^ 2 + (PlaneTree.bienayme μ).real {T : PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ G T ∧ ∃ U ∈ T.fringeTrees[ℓ]?, G U}

Two-start bound (P11), in ℝ and with the cyclic indicator I_{1+ℓ}^{(M)}: for ℓ + M ≤ N, P(I_1^{(M)} = 1, I_{1+ℓ}^{(M)} = 1) ≤ P(G(𝒯) = 1)² + A(ℓ), where A(ℓ) = P(|𝒯| ≥ ℓ + 1, G(𝒯) = 1, G(𝒯_{u_{ℓ+1}}) = 1).

theorem PoissonDeclumping.Bridge.walkVecLaw_real_pair_le_markProb (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) (n : ℕ) {M N ℓ : ℕ} (hN : ℓ + M ≤ N) : (Lukasiewicz.walkVecLaw μ N).real {ω : Fin N → ℤ | Cyclic.FirstMarked (G (k n)) (↑M) (List.ofFn ω) ∧ Cyclic.FirstMarked (G (k n)) (↑M) ((List.ofFn ω).rotate ℓ)} ≤ markProb μ G k n ^ 2 + pairProb μ G k n ℓ

Lemma lem:boundb2, unconditioned two-start bound (source line 1843), in the paper's notation: for ℓ + M ≤ N, P(I_1^{(M)} = 1, I_{1+ℓ}^{(M)} = 1) ≤ π_n² + A_n(ℓ) with G = G_{k_n}.