The probabilities q and p, the truncation coupling, and the strong Markov property at ζ

Work package WP4 (remainder) of the bridge plan (no toolkit). Source lines 1683–1696 (q_n, proof of Lemma lem:truncate), 1720–1728 (cyclic invariance of q_n), 1736–1760 (p_n, proof of Lemma lem:pnqn(i)), 1781 (uniform-vertex representation of q_n).

The indicators are those of Cyclic/Indicators.lean: FirstMarked G M 𝐱 is I_1^{(M)}(𝐱) = 1, (List.ofFn ω).rotate i is the i-th cyclic shift, cyclicSum G M (List.ofFn ω) is W_n^M = ∑_{i ≤ n} I_i^{(M)}(X_1, …, X_n). For the paper's quantities take G = G_{k_n} and M = M_n.

Main statements

• qProb μ G M n = P(I_1^{(M)}(X_1..X_n) = 1 | S_n = -1) and pProb μ G M = P(I_1^{(M)}(X_1..X_M) = 1).
• qProb_eq_uniformFringeLaw: q = P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| ≤ M); bridgeLaw_real_firstMarked_rotate, bridgeLaw_real_shiftIndicator_eq_one: every cyclic indicator has bridge probability q; firstMarked_rotate_iff_drop: non-cyclic form.
• P09: cyclicSum_le_cyclicSum_length (W_n^M ≤ W_n^n), integral_cyclicSum_sub_truncated (E[W_n^n - W_n^M | S_n = -1] = n P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| > M)) and the coupling bound paperTVDist_cyclicSum_truncated_le.
• Strong Markov property at ζ: walkVecLaw_zeta_eq_inter_drop (fresh increments after ζ = j), pProb_eq (p = P(G(𝒯) = 1, |𝒯| ≤ M)), walkVecLaw_firstMarked_eq_pProb, pProb_le, and the endpoint bound walkVecLaw_firstMarked_abs_sum_gt_le: P(I_1^{(M)} = 1, |S_M| > r) ≤ ∑_{j=1}^{M} P(G(𝒯) = 1, |𝒯| = j) P(|S_{M-j}| > r - 1).

All statements hold for every n (at inadmissible n the bridge law is 0).

The probabilities q_n and p_n

noncomputable def PoissonDeclumping.Bridge.qProb (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : ℝ

q = P(I_1^{(M)}(X_1, …, X_n) = 1 | S_n = -1) (source lines 1683, 1724; with M = M_n and G = G_{k_n} this is the paper's q_n).

Equations

• PoissonDeclumping.Bridge.qProb μ G M n = (PoissonDeclumping.Lukasiewicz.bridgeLaw μ n).real {ω : Fin n → ℤ | PoissonDeclumping.Cyclic.FirstMarked G (↑M) (List.ofFn ω)}

noncomputable def PoissonDeclumping.Bridge.pProb (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ) : ℝ

p = P(I_1^{(M)}(X_1, …, X_M) = 1) (source line 1736; the paper's p_n for M = M_n). By locality of I_1^{(M)} it is also P(I_1^{(M)}(X_1, …, X_n) = 1) for every n ≥ M (walkVecLaw_firstMarked_eq_pProb).

Equations

• PoissonDeclumping.Bridge.pProb μ G M = (PoissonDeclumping.Lukasiewicz.walkVecLaw μ M).real {ω : Fin M → ℤ | PoissonDeclumping.Cyclic.FirstMarked G (↑M) (List.ofFn ω)}

instance PoissonDeclumping.Bridge.instIsZeroOrProbabilityMeasureBridgeLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsZeroOrProbabilityMeasure (Lukasiewicz.bridgeLaw μ n)

theorem PoissonDeclumping.Bridge.isProbabilityMeasure_bridgeLaw {μ : PMF ℕ} {n : ℕ} (h : PlaneTree.Admissible μ n) : MeasureTheory.IsProbabilityMeasure (Lukasiewicz.bridgeLaw μ n)

instance PoissonDeclumping.Bridge.instIsFiniteMeasureUniformFringeLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsFiniteMeasure (uniformFringeLaw μ n)

theorem PoissonDeclumping.Bridge.setOf_firstIndicator_eq_one (G : PlaneTree → Prop) (M : ℕ∞) {n : ℕ} : {ω : Fin n → ℤ | Cyclic.firstIndicator G M (List.ofFn ω) = 1} = {ω : Fin n → ℤ | Cyclic.FirstMarked G M (List.ofFn ω)}

theorem PoissonDeclumping.Bridge.qProb_eq_uniformFringeLaw (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : qProb μ G M n = (uniformFringeLaw μ n).real {T : PlaneTree | G T ∧ T.vertexCount ≤ M}

q = P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| ≤ M) (source lines 1695, 1781): the uniform-vertex representation of q.

theorem PoissonDeclumping.Bridge.bridgeLaw_real_firstMarked_rotate (μ : PMF ℕ) (G : PlaneTree → Prop) (M n i : ℕ) : (Lukasiewicz.bridgeLaw μ n).real {ω : Fin n → ℤ | Cyclic.FirstMarked G (↑M) ((List.ofFn ω).rotate i)} = qProb μ G M n

Cyclic invariance of q (source line 1724): every cyclic indicator I_{i+1}^{(M)}(X_1, …, X_n) has bridge probability q.

theorem PoissonDeclumping.Bridge.bridgeLaw_real_shiftIndicator_eq_one (μ : PMF ℕ) (G : PlaneTree → Prop) (M n i : ℕ) : (Lukasiewicz.bridgeLaw μ n).real {ω : Fin n → ℤ | Cyclic.shiftIndicator G (↑M) (List.ofFn ω) i = 1} = qProb μ G M n

The same in the firstIndicator/shiftIndicator language of Cyclic/Indicators.lean.

theorem PoissonDeclumping.Bridge.firstMarked_rotate_iff_drop {G : PlaneTree → Prop} {x : List ℤ} {i M : ℕ} (h : i + M ≤ x.length) : Cyclic.FirstMarked G (↑M) (x.rotate i) ↔ Cyclic.FirstMarked G (↑M) (List.drop i x)

Before the wrap-around, I_{i+1}^{(M)} only reads x_{i+1}, …, x_{i+M}: if i + M ≤ |𝐱|, then I_{i+1}^{(M)}(𝐱) = I_1^{(M)}(x_{i+1}, …, x_n) (non-cyclic form).

The truncation coupling (P09, Lemma lem:truncate(i), source lines 1692–1693)

theorem PoissonDeclumping.Bridge.cyclicSum_le_length (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) : Cyclic.cyclicSum G M x ≤ x.length

theorem PoissonDeclumping.Bridge.cyclicSum_le_cyclicSum_length {n : ℕ} (G : PlaneTree → Prop) (M : ℕ∞) (ω : Fin n → ℤ) : Cyclic.cyclicSum G M (List.ofFn ω) ≤ Cyclic.cyclicSum G (↑n) (List.ofFn ω)

0 ≤ W_n^M ≤ W_n^n: the truncated count is at most the full count, for every cutoff.

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

E[∑_{i ≤ n} I_i^{(M)} | S_n = -1] = n P(I_1^{(M)} = 1 | S_n = -1), in ℝ.

theorem PoissonDeclumping.Bridge.integrable_cyclicSum_bridgeLaw (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ∞) (n : ℕ) : MeasureTheory.Integrable (fun (ω : Fin n → ℤ) => ↑(Cyclic.cyclicSum G M (List.ofFn ω))) (Lukasiewicz.bridgeLaw μ n)

theorem PoissonDeclumping.Bridge.integral_cyclicSum_sub_truncated (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : ∫ (ω : Fin n → ℤ), ↑(Cyclic.cyclicSum G (↑n) (List.ofFn ω)) - ↑(Cyclic.cyclicSum G (↑M) (List.ofFn ω)) ∂Lukasiewicz.bridgeLaw μ n = ↑n * (uniformFringeLaw μ n).real {T : PlaneTree | G T ∧ M < T.vertexCount}

P09 (source lines 1692–1693): E[W_n^n - W_n^M | S_n = -1] = n P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| > M).

theorem PoissonDeclumping.Bridge.paperTVDist_cyclicSum_truncated_le (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : paperTVDist (MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Cyclic.cyclicSum G (↑M) (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n)) (MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Cyclic.cyclicSum G (↑n) (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n)) ≤ ↑n * (uniformFringeLaw μ n).real {T : PlaneTree | G T ∧ M < T.vertexCount}

Truncation coupling (Lemma lem:truncate(i), source lines 1692–1693): the laws of the truncated count W_n^M = ∑_i I_i^{(M)} and of the full count W_n^n under P(· | S_n = -1) are within n P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| > M) in total variation.

The strong Markov property at ζ (source lines 1753–1760)

theorem PoissonDeclumping.Bridge.walkVecLaw_zeta_eq_inter_drop (μ : PMF ℕ) {j n : ℕ} (hj : j ≤ n) (A : Set PlaneTree) (K : List ℤ → Prop) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | Lukasiewicz.zeta (List.ofFn ω) = some j ∧ (∃ T ∈ A, PlaneTree.ofSeq (List.ofFn ω) = some T) ∧ K (List.drop j (List.ofFn ω))} = (PlaneTree.bienayme μ) (A ∩ {T : PlaneTree | T.vertexCount = j}) * (Lukasiewicz.walkVecLaw μ (n - j)) {b : Fin (n - j) → ℤ | K (List.ofFn b)}

Strong Markov property at ζ, fresh increments. For j ≤ n, P(ζ = j, T(𝐗) ∈ A, K(X_{j+1}, …, X_n)) = P(𝒯 ∈ A, |𝒯| = j) P(K(X_1, …, X_{n-j})).

theorem PoissonDeclumping.Bridge.pProb_eq (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ) : pProb μ G M = (PlaneTree.bienayme μ).real {T : PlaneTree | G T ∧ T.vertexCount ≤ M}

p = P(G(𝒯) = 1, |𝒯| ≤ M) (source lines 1753–1760, last sentence of the proof of Lemma lem:pnqn(i): ∑_{j ≤ M} E[I_1^{(M)} 1_{ζ = j}] = p).

theorem PoissonDeclumping.Bridge.walkVecLaw_firstMarked_eq_pProb (μ : PMF ℕ) (G : PlaneTree → Prop) {M n : ℕ} (hM : M ≤ n) : (Lukasiewicz.walkVecLaw μ n).real {ω : Fin n → ℤ | Cyclic.FirstMarked G (↑M) (List.ofFn ω)} = pProb μ G M

Locality: P(I_1^{(M)}(X_1, …, X_n) = 1) = p for every n ≥ M.

theorem PoissonDeclumping.Bridge.pProb_le (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ) : pProb μ G M ≤ (PlaneTree.bienayme μ).real {T : PlaneTree | G T}

p ≤ π: P(I_1^{(M)} = 1) ≤ P(G(𝒯) = 1).

theorem PoissonDeclumping.Bridge.walkVecLaw_firstMarked_abs_sum_gt_le (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ) (r : ℝ) : (Lukasiewicz.walkVecLaw μ M).real {ω : Fin M → ℤ | Cyclic.FirstMarked G (↑M) (List.ofFn ω) ∧ r < |↑(∑ i : Fin M, ω i)|} ≤ ∑ j ∈ Finset.Icc 1 M, (PlaneTree.bienayme μ).real {T : PlaneTree | G T ∧ T.vertexCount = j} * (walkLaw μ (M - j)).real {x : ℤ | r - 1 < |↑x|}

Endpoint bound at ζ (source lines 1753–1760): decomposing according to ζ = j ≤ M and using the fresh increments after ζ, P(I_1^{(M)} = 1, |S_M| > r) ≤ ∑_{j=1}^{M} P(G(𝒯) = 1, |𝒯| = j) P(|S_{M-j}| > r - 1).