Endpoint smoothing: Lemma lem:1 and Proposition prop:b3bis (b_3 → 0)

Work package WP6 of the bridge plan. Source lines 1860–1995 (Proposition 4.8, Lemma 4.9; inventory P12, B14). Notation: I_j^{(M)} are the cyclic indicators of Bridge/ErrorTerms.lean (cycEvent), q_n = qProb, p_n = pProb, π_n = markProb, Ψ_m = walkProb μ m, r_n = √(a_{M_n} a_n), and b_3 = errorB3 is the third Chen–Stein error term of ChenStein.prop_AGG for the bridge P(· | S_n = -1).

• windowCount G M K y = ∑_{j=0}^{K-M} I_1^{(M)}(y_{j+1}, …) counts the indicators reading only y_1, …, y_K; windowMean μ G M K N f s = E[f(1 + windowCount K) | S_N = s], and the paper's h_n(k) = E[f(1 + ∑_{j=1}^{n-2M_n+1} I_j^{(M_n)}) | S_{n-M_n} = -1-k] (source line 1873) is endpointMean μ G M n f k = windowMean μ G M (n-M) (n-M) f (-1-k).

Main statements

• errorB3_eq_mul, sum_compl_cycNbhd_indicator (cyclic exchangeability and the bookkeeping of the cyclic wrap, source lines 1873–1880): the indices outside B_i are those at forward distance M, …, n - M, and b_3 = n |E[(I_1 - q) f(1 + ∑_{j ≤ n-2M+1} I_{M+j}) | S_n = -1]|.
• integral_blockIntegrand_eq (block reduction, source lines 1880–1886): conditional independence of (X_1..X_M) and (X_{M+1}..X_n) given S_M, S_n, and subtraction of any constant κ from h_n (as E[I_1 - q | S_n = -1] = 0).
• integral_cond_take (Markov property at a deterministic time for bounded functions), cond_walkVecLaw_real_firstMarked_drop (exchangeability of the conditioned walk), abs_windowMean_sub_le (deletion estimate eq:hne), abs_walkProb_div_sub_div_le and abs_windowMean_sub_windowMean_le (deterministic endpoint smoothing).
• eventually_abs_endpointMean_sub_le (corrected eq:delta_vanish, via eq:approx1 and eq:approx3): uniformly in ‖f‖_∞ ≤ 1 and in compatible endpoints k, k' with |k|, |k'| ≤ r_n, |h_n(k) - h_n(k')| → 0.
• exists_eventually_mul_abs_integral_le (the split |S_{M_n}| ≤ r_n / > r_n and the bounds on R_n^1, R_n^2), eventually_lem1, tendsto_lem1 (Lemma lem:1, with a compatible base point).
• eventually_errorB3_le (Proposition prop:b3bis, uniform in the test function, which is what exists_paperTVDist_cyclicSum_le_errorTerms requires) and tendsto_errorB3.

Departures from the source

• Periodic laws (correction F2). The paper's Δ_n(k) = h_n(k) - h_n(0) conditions on S_{n-M_n} = -1, a null event unless d ∣ M_n (d the span; admissible n have d ∣ n - 1). Here the base value is h_n(k₀) for a compatible k₀ (Ψ_{n-M_n}(-1-k₀) ≠ 0, |k₀| ≤ r_n), and eq:delta_vanish is proved as an oscillation bound over pairs of compatible endpoints. S_{M_n} is compatible almost surely under the bridge; at incompatible endpoints the weight Ψ_{n-M_n}(-1-S_{M_n}) vanishes.
• No Skorokhod representation (correction F7). eq:approx3 is proved by the deterministic bound |Ψ_t(s-y)/Ψ_N(s) - Ψ_t(s'-y)/Ψ_N(s')| ≤ (a_N/a_t)(2δ₁/L + 8Cδ₂/L²), uniform in y, from LatticeLocal.equicont at time t = ⌊εn⌋, eventually_abs_mul_sub_le at time N = n - M_n and sup_le; the small time fraction ε is chosen first, from the target.
• Marginal tightness (F6) replaces convergence in law of S_{M_n}/a_{M_n} (line 1912).
• The large-endpoint term and the small-endpoint term are bounded directly in walk form (Markov property at time M_n under the bridge) with Ψ_{n-M_n} ≤ C/a_n, Ψ_n(-1) ≥ c/a_n, instead of Lemma lem:error_est; eq:approx1 uses Lemma lem:error_est with N_n = n - M_n, z_n = 1 + r_n and p_n ≤ π_n (instead of p_n ≤ C q_n).
• Assumption (M) is not used: Proposition prop:b3bis holds under bounded n π_n and the cutoff properties alone.

def PoissonDeclumping.Bridge.markSet (G : PlaneTree → Prop) (M : ℕ) : Set (List ℤ)

The event {I_1^{(M)}(𝐱) = 1} on sequences.

Equations

• PoissonDeclumping.Bridge.markSet G M = {x : List ℤ | PoissonDeclumping.Cyclic.FirstMarked G (↑M) x}

noncomputable def PoissonDeclumping.Bridge.windowCount (G : PlaneTree → Prop) (M K : ℕ) (y : List ℤ) : ℕ

∑_{j=0}^{K-M} I_1^{(M)}(y_{j+1}, y_{j+2}, …): the indicators that read only the window (y_1, …, y_K).

Equations

• PoissonDeclumping.Bridge.windowCount G M K y = ∑ j ∈ Finset.range (K + 1 - M), (PoissonDeclumping.Bridge.markSet G M).indicator 1 (List.drop j y)

noncomputable def PoissonDeclumping.Bridge.windowMean (μ : PMF ℕ) (G : PlaneTree → Prop) (M K N : ℕ) (f : ℕ → ℝ) (s : ℤ) : ℝ

E[f(1 + ∑_{j=0}^{K-M} I_{j+1}^{(M)}) | S_N = s].

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PoissonDeclumping.Bridge.endpointMean (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) (f : ℕ → ℝ) (k : ℤ) : ℝ

The paper's h_n(k) = E[f(1 + ∑_{j=1}^{n-2M+1} I_j^{(M)}) | S_{n-M} = -1-k] (source line 1873, with M = M_n): the indicators of the second block (X_{M+1}, …, X_n), of length n - M, given its sum -1 - k. It is 0 at a null endpoint (cond of a null event).

Equations

• PoissonDeclumping.Bridge.endpointMean μ G M n f k = PoissonDeclumping.Bridge.windowMean μ G M (n - M) (n - M) f (-1 - k)

theorem PoissonDeclumping.Bridge.indicator_markSet_eq {X : Type u_1} (G : PlaneTree → Prop) (M : ℕ) (g : X → List ℤ) (x : X) {R : Type u_2} [Zero R] [One R] : (markSet G M).indicator 1 (g x) = {x : X | Cyclic.FirstMarked G (↑M) (g x)}.indicator 1 x

Rewriting 1_{I_1^{(M)}(g(x)) = 1} as the indicator of an event in x.

Rotation invariance of the conditioned walk

theorem PoissonDeclumping.Bridge.map_cond_walkVecLaw_comp_perm (μ : PMF ℕ) {N : ℕ} (s : ℤ) (σ : Equiv.Perm (Fin N)) : MeasureTheory.Measure.map (fun (ω : Fin N → ℤ) => ω ∘ ⇑σ) (Lukasiewicz.walkVecLaw μ N)[|{ω : Fin N → ℤ | ∑ i : Fin N, ω i = s}] = (Lukasiewicz.walkVecLaw μ N)[|{ω : Fin N → ℤ | ∑ i : Fin N, ω i = s}]

The law of (X_1, …, X_N) given S_N = s is invariant under permutations of the coordinates.

theorem PoissonDeclumping.Bridge.cond_walkVecLaw_real_rotate (μ : PMF ℕ) (N j : ℕ) (s : ℤ) (P : List ℤ → Prop) : (Lukasiewicz.walkVecLaw μ N)[|{ω : Fin N → ℤ | ∑ i : Fin N, ω i = s}].real {ω : Fin N → ℤ | P ((List.ofFn ω).rotate j)} = (Lukasiewicz.walkVecLaw μ N)[|{ω : Fin N → ℤ | ∑ i : Fin N, ω i = s}].real {ω : Fin N → ℤ | P (List.ofFn ω)}

Cyclic exchangeability of (X_1, …, X_N) given S_N = s, event form.

theorem PoissonDeclumping.Bridge.cond_walkVecLaw_real_firstMarked_drop (μ : PMF ℕ) (G : PlaneTree → Prop) {M N j : ℕ} (h : j + M ≤ N) (s : ℤ) : (Lukasiewicz.walkVecLaw μ N)[|{ω : Fin N → ℤ | ∑ i : Fin N, ω i = s}].real {ω : Fin N → ℤ | Cyclic.FirstMarked G (↑M) (List.drop j (List.ofFn ω))} = (Lukasiewicz.walkVecLaw μ N)[|{ω : Fin N → ℤ | ∑ i : Fin N, ω i = s}].real {ω : Fin N → ℤ | Cyclic.FirstMarked G (↑M) (List.take M (List.ofFn ω))}

Exchangeability of the conditioned walk for the indicators: for j + M ≤ N, P(I_{j+1}^{(M)} = 1 | S_N = s) = P(I_1^{(M)} = 1 | S_N = s).

The Markov property at a deterministic time, for bounded functions

theorem PoissonDeclumping.Bridge.integral_cond_take (μ : PMF ℕ) {m N : ℕ} (hmN : m ≤ N) (s : ℤ) (Φ : List ℤ → ℝ) {C : ℝ} (hΦ : ∀ (x : List ℤ), |Φ x| ≤ C) : ∫ (ω : Fin N → ℤ), Φ (List.take m (List.ofFn ω)) ∂(Lukasiewicz.walkVecLaw μ N)[|{ω : Fin N → ℤ | ∑ i : Fin N, ω i = s}] = (walkProb μ (↑N) s)⁻¹ * ∫ (a : Fin m → ℤ), Φ (List.ofFn a) * walkProb μ (↑(N - m)) (s - ∑ i : Fin m, a i) ∂Lukasiewicz.walkVecLaw μ m

Markov property at the deterministic time m, integral form: for a bounded Φ and m ≤ N, E[Φ(X_1..X_m) | S_N = s] = Ψ_N(s)⁻¹ E[Φ(X_1..X_m) Ψ_{N-m}(s - S_m)].

The window counts

theorem PoissonDeclumping.Bridge.mem_markSet_drop_take_iff {G : PlaneTree → Prop} {M K j : ℕ} {y : List ℤ} (h : j + M ≤ K) : List.drop j (List.take K y) ∈ markSet G M ↔ List.drop j y ∈ markSet G M

I_{j+1}^{(M)} of (y_1, …, y_K) agrees with that of y when j + M ≤ K.

theorem PoissonDeclumping.Bridge.windowCount_take (G : PlaneTree → Prop) (M K : ℕ) (y : List ℤ) : windowCount G M K (List.take K y) = windowCount G M K y

Locality: the window count of (y_1, …, y_K) only reads y_1, …, y_K.

theorem PoissonDeclumping.Bridge.windowCount_eq_add (G : PlaneTree → Prop) (M : ℕ) {K' K : ℕ} (h : K' ≤ K) (y : List ℤ) : windowCount G M K y = windowCount G M K' y + ∑ j ∈ Finset.Ico (K' + 1 - M) (K + 1 - M), (markSet G M).indicator 1 (List.drop j y)

Shrinking the window deletes the indicators I_{j+1}, K' + 1 - M ≤ j < K + 1 - M.

theorem PoissonDeclumping.Bridge.abs_windowMean_sub_le (μ : PMF ℕ) (G : PlaneTree → Prop) (M N : ℕ) {K' K : ℕ} (h : K' ≤ K) {f : ℕ → ℝ} (hf : ∀ (w : ℕ), |f w| ≤ 1) (s : ℤ) : |windowMean μ G M K N f s - windowMean μ G M K' N f s| ≤ 2 * ∑ j ∈ Finset.Ico (K' + 1 - M) (K + 1 - M), (Lukasiewicz.walkVecLaw μ N)[|{b : Fin N → ℤ | ∑ i : Fin N, b i = s}].real {b : Fin N → ℤ | Cyclic.FirstMarked G (↑M) (List.drop j (List.ofFn b))}

Deletion estimate (source line eq:hne): removing the indicators I_{j+1}, K' + 1 - M ≤ j < K + 1 - M, from the argument of f changes the conditional mean by at most 2 ∑_j P(I_{j+1} = 1 | S_N = s).

Endpoint smoothing at a fixed size

theorem PoissonDeclumping.Bridge.windowMean_eq (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ) {K N : ℕ} (hKN : K ≤ N) {f : ℕ → ℝ} (hf : ∀ (w : ℕ), |f w| ≤ 1) (s : ℤ) : windowMean μ G M K N f s = (walkProb μ (↑N) s)⁻¹ * ∫ (a : Fin K → ℤ), f (1 + windowCount G M K (List.ofFn a)) * walkProb μ (↑(N - K)) (s - ∑ i : Fin K, a i) ∂Lukasiewicz.walkVecLaw μ K

The Markov property at time K for the window mean: for K ≤ N, E[f(1 + W_K) | S_N = s] = Ψ_N(s)⁻¹ E[f(1 + W_K) Ψ_{N-K}(s - S_K)].

theorem PoissonDeclumping.Bridge.abs_walkProb_div_sub_div_le {μ : PMF ℕ} {a : ℕ → ℝ} {d : ℕ} {L : ℝ} (hloc : LatticeLocal μ a d L) {t N : ℕ} {s s' : ℤ} {δ₁ δ₂ C η : ℝ} (hat : 0 < a t) (haN : 0 < a N) (hs : |a N * walkProb μ (↑N) s - L| ≤ δ₂) (hs' : |a N * walkProb μ (↑N) s' - L| ≤ δ₂) (hδ₂ : δ₂ ≤ L / 2) (hδ₁ : 0 ≤ δ₁) (hds : ↑d ∣ s - s') (heq : ∀ (x y : ℤ), ↑d ∣ x + ↑t → ↑d ∣ y + ↑t → |↑(x - y)| ≤ η * a t → |a t * walkProb μ (↑t) x - a t * walkProb μ (↑t) y| ≤ δ₁) (hss' : |↑(s - s')| ≤ η * a t) (hsup : ∀ (x : ℤ), walkProb μ (↑t) x ≤ C / a t) (y : ℤ) : |walkProb μ (↑t) (s - y) / walkProb μ (↑N) s - walkProb μ (↑t) (s' - y) / walkProb μ (↑N) s'| ≤ a N / a t * (2 * δ₁ / L + 8 * C * δ₂ / L ^ 2)

The deterministic endpoint-smoothing bound (replacing Skorokhod's representation and dominated convergence at source lines 1987–1994, correction F7): uniformly in the position y, |Ψ_t(s - y)/Ψ_N(s) - Ψ_t(s' - y)/Ψ_N(s')| ≤ (a_N / a_t) (2δ₁/L + 8Cδ₂/L²) when a_N Ψ_N(s), a_N Ψ_N(s') are δ₂-close to L, s ≡ s' (mod d), |s - s'| is within the equicontinuity range at time t, and a_t Ψ_t ≤ C.

theorem PoissonDeclumping.Bridge.abs_windowMean_sub_windowMean_le (μ : PMF ℕ) (G : PlaneTree → Prop) (M : ℕ) {t N : ℕ} (htN : t ≤ N) {f : ℕ → ℝ} (hf : ∀ (w : ℕ), |f w| ≤ 1) {s s' : ℤ} {B : ℝ} (hB : ∀ (y : ℤ), |walkProb μ (↑t) (s - y) / walkProb μ (↑N) s - walkProb μ (↑t) (s' - y) / walkProb μ (↑N) s'| ≤ B) : |windowMean μ G M (N - t) N f s - windowMean μ G M (N - t) N f s'| ≤ B

Smoothing step (proof of eq:approx3): a uniform bound on the ratio difference bounds the difference of the window means after cutting the last t steps.

The oscillation of h_n over compatible endpoints

theorem PoissonDeclumping.Bridge.isLittleO_one_add_sqrt {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {M : ℕ → ℕ} (hM : IsCutoff M) : (fun (n : ℕ) => 1 + √(a (M n) * a n)) =o[Filter.atTop] fun (n : ℕ) => a (n - M n)

1 + r_n = o(a_{n - M_n}) for r_n = √(a_{M_n} a_n).

theorem PoissonDeclumping.Bridge.eventually_abs_endpointMean_sub_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in admissibleSizes μ, ∀ (f : ℕ → ℝ), (∀ (w : ℕ), |f w| ≤ 1) → ∀ (x x' : ℤ), |↑x| ≤ √(a (M n) * a n) → |↑x'| ≤ √(a (M n) * a n) → walkProb μ (↑(n - M n)) (-1 - x) ≠ 0 → walkProb μ (↑(n - M n)) (-1 - x') ≠ 0 → |endpointMean μ (G (k n)) (M n) n f x - endpointMean μ (G (k n)) (M n) n f x'| ≤ ε

The endpoint oscillation of h_n vanishes (corrected eq:delta_vanish, source lines 1925–1995; corrections F2, F7): uniformly over test functions ‖f‖_∞ ≤ 1 and over pairs of compatible endpoints k, k' with |k|, |k'| ≤ r_n = √(a_{M_n} a_n), |h_n(k) - h_n(k')| → 0 along admissible sizes. Compatibility (Ψ_{n-M_n}(-1-k) ≠ 0) replaces the paper's base point 0, which is a null endpoint unless d ∣ M_n (periodic case). Only the cutoff properties and bounded n π_n are used.

Block reduction of b_3

theorem PoissonDeclumping.Bridge.integral_bridgeLaw_rotate (μ : PMF ℕ) (n i : ℕ) (Φ : List ℤ → ℝ) : ∫ (ω : Fin n → ℤ), Φ ((List.ofFn ω).rotate i) ∂Lukasiewicz.bridgeLaw μ n = ∫ (ω : Fin n → ℤ), Φ (List.ofFn ω) ∂Lukasiewicz.bridgeLaw μ n

Cyclic exchangeability of the bridge, integral form.

theorem PoissonDeclumping.Bridge.image_cycGap_compl_cycNbhd {M n : ℕ} (hM : 0 < M) (i : Fin n) : Finset.image (fun (j : Fin n) => cycGap n ↑i ↑j) (Finset.univ \ cycNbhd n M i) = Finset.Icc M (n - M)

The forward gaps cycGap n i j of the indices j outside the neighbourhood B_i are exactly M, …, n - M.

theorem PoissonDeclumping.Bridge.sum_compl_cycNbhd_indicator (G : PlaneTree → Prop) {M n : ℕ} (hM : 0 < M) (ω : Fin n → ℤ) (i : Fin n) : ∑ j ∈ Finset.univ \ cycNbhd n M i, (cycEvent G M n j).indicator 1 ω = windowCount G M (n - M) (List.drop M ((List.ofFn ω).rotate ↑i))

Bookkeeping of the cyclic wrap (source lines 1873–1880): the indices outside the neighbourhood B_i are those at forward distance M, …, n - M from i, so ∑_{j ∉ B_i} I_j^{(M)}(𝐱) is the window count of the block (x_{i+M+1}, …, x_{i+n}) of the i-th cyclic shift (n - M increments, n - 2M + 1 indicators).

noncomputable def PoissonDeclumping.Bridge.blockIntegrand (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) (f : ℕ → ℝ) (y : List ℤ) : ℝ

The integrand (I_1^{(M)}(𝐲) - q) f(1 + ∑_{j=1}^{n-2M+1} I_{M+j}^{(M)}(𝐲)) of the reduced form of b_3 (source line 1877).

Equations

• One or more equations did not get rendered due to their size.

theorem PoissonDeclumping.Bridge.errorB3_integrand_eq (μ : PMF ℕ) (G : PlaneTree → Prop) {M n : ℕ} (hM : 0 < M) (f : ℕ → ℝ) (i : Fin n) (ω : Fin n → ℤ) : ((cycEvent G M n i).indicator 1 ω - (Lukasiewicz.bridgeLaw μ n).real (cycEvent G M n i)) * f (1 + ∑ j ∈ Finset.univ \ cycNbhd n M i, (cycEvent G M n j).indicator 1 ω) = blockIntegrand μ G M n f ((List.ofFn ω).rotate ↑i)

The integrand of b_3 at index i, as a function of the i-th cyclic shift.

theorem PoissonDeclumping.Bridge.errorB3_eq_mul (μ : PMF ℕ) (G : PlaneTree → Prop) {M n : ℕ} (hM : 0 < M) (f : ℕ → ℝ) : errorB3 μ G M n f = ↑n * |∫ (ω : Fin n → ℤ), blockIntegrand μ G M n f (List.ofFn ω) ∂Lukasiewicz.bridgeLaw μ n|

Cyclic exchangeability for b_3 (source line 1877): all n terms of b_3 are equal, b_3 = n |E[(I_1^{(M)} - q) f(1 + ∑_{j ≤ n - 2M + 1} I_{M+j}^{(M)}) | S_n = -1]|.

Subtracting a compatible base value and returning to the walk

theorem PoissonDeclumping.Bridge.abs_endpointMean_le (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) {f : ℕ → ℝ} (hf : ∀ (w : ℕ), |f w| ≤ 1) (x : ℤ) : |endpointMean μ G M n f x| ≤ 1

|h_n(k)| ≤ ‖f‖_∞ ≤ 1 (also at null endpoints, where h_n(k) = 0).

theorem PoissonDeclumping.Bridge.abs_indicator_sub_qProb_le (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) (y : List ℤ) : |(markSet G M).indicator 1 y - qProb μ G M n| ≤ 1

|I_1^{(M)} - q| ≤ 1.

theorem PoissonDeclumping.Bridge.indicator_markSet_take (G : PlaneTree → Prop) (M : ℕ) (y : List ℤ) : (markSet G M).indicator 1 (List.take M y) = (markSet G M).indicator 1 y

Locality of I_1^{(M)}: it only reads the first M entries.

theorem PoissonDeclumping.Bridge.integral_blockIntegrand_eq (μ : PMF ℕ) (G : PlaneTree → Prop) {M n : ℕ} (hn : PlaneTree.Admissible μ n) (hMn : M ≤ n) {f : ℕ → ℝ} (hf : ∀ (w : ℕ), |f w| ≤ 1) (κ : ℝ) : ∫ (ω : Fin n → ℤ), blockIntegrand μ G M n f (List.ofFn ω) ∂Lukasiewicz.bridgeLaw μ n = ∫ (ω : Fin n → ℤ), ((markSet G M).indicator 1 (List.ofFn ω) - qProb μ G M n) * (endpointMean μ G M n f (List.take M (List.ofFn ω)).sum - κ) ∂Lukasiewicz.bridgeLaw μ n

Block reduction of b_3 (proof of Proposition prop:b3bis, source lines 1880–1886): conditionally on S_{M} = k and S_n = -1, the blocks (X_1..X_M) and (X_{M+1}..X_n) are independent, so E[(I_1 - q) f(1 + ∑_j I_{M+j}) | S_n = -1] = E[(I_1 - q) h_n(S_M) | S_n = -1]; since E[I_1 - q | S_n = -1] = 0, any constant κ may be subtracted from h_n (correction F2: the paper subtracts h_n(0), a conditional mean at a null endpoint in the periodic case).

theorem PoissonDeclumping.Bridge.integral_bridgeLaw_eq_walk (μ : PMF ℕ) (G : PlaneTree → Prop) {M n : ℕ} (hMn : M ≤ n) {f : ℕ → ℝ} (hf : ∀ (w : ℕ), |f w| ≤ 1) (κ : ℝ) : ∫ (ω : Fin n → ℤ), ((markSet G M).indicator 1 (List.ofFn ω) - qProb μ G M n) * (endpointMean μ G M n f (List.take M (List.ofFn ω)).sum - κ) ∂Lukasiewicz.bridgeLaw μ n = (walkProb μ (↑n) (-1))⁻¹ * ∫ (b : Fin M → ℤ), ((markSet G M).indicator 1 (List.ofFn b) - qProb μ G M n) * (endpointMean μ G M n f (∑ i : Fin M, b i) - κ) * walkProb μ (↑(n - M)) (-1 - ∑ i : Fin M, b i) ∂Lukasiewicz.walkVecLaw μ M

Markov property at time M under the bridge: the reduced b_3 integrand in walk form, E[(I_1 - q)(h_n(S_M) - κ) | S_n = -1] = Ψ_n(-1)⁻¹ E[(I_1 - q)(h_n(S_M) - κ) Ψ_{n-M}(-1 - S_M)].

The final estimate

theorem PoissonDeclumping.Bridge.walkVecLaw_real_abs_sum_gt (μ : PMF ℕ) (m : ℕ) (r : ℝ) : (Lukasiewicz.walkVecLaw μ m).real {b : Fin m → ℤ | r < |↑(∑ i : Fin m, b i)|} = (walkLaw μ m).real {x : ℤ | r < |↑x|}

P(|S_m| > r) computed from the increments.

theorem PoissonDeclumping.Bridge.abs_walkIntegral_le (μ : PMF ℕ) (G : PlaneTree → Prop) {M n : ℕ} {f : ℕ → ℝ} (hf : ∀ (w : ℕ), |f w| ≤ 1) {κ ε' r B : ℝ} (hκ : |κ| ≤ 1) (hε' : 0 ≤ ε') (hosc : ∀ (x : ℤ), |↑x| ≤ r → walkProb μ (↑(n - M)) (-1 - x) ≠ 0 → |endpointMean μ G M n f x - κ| ≤ ε') (hB : ∀ (x : ℤ), walkProb μ (↑(n - M)) x ≤ B) : |∫ (b : Fin M → ℤ), ((markSet G M).indicator 1 (List.ofFn b) - qProb μ G M n) * (endpointMean μ G M n f (∑ i : Fin M, b i) - κ) * walkProb μ (↑(n - M)) (-1 - ∑ i : Fin M, b i) ∂Lukasiewicz.walkVecLaw μ M| ≤ B * (ε' * (pProb μ G M + qProb μ G M n) + 2 * (Lukasiewicz.walkVecLaw μ M).real {b : Fin M → ℤ | Cyclic.FirstMarked G (↑M) (List.ofFn b) ∧ r < |↑(∑ i : Fin M, b i)|} + 2 * qProb μ G M n * (Lukasiewicz.walkVecLaw μ M).real {b : Fin M → ℤ | r < |↑(∑ i : Fin M, b i)|})

The small/large endpoint split (proof of Lemma lem:1, bounds on R_n^1, R_n^2, source lines 1898–1924), at a fixed size: if |h_n(k) - κ| ≤ ε' at every compatible endpoint |k| ≤ r, |κ| ≤ 1 and Ψ_{n-M} ≤ B, then |E[(I_1 - q)(h_n(S_M) - κ) Ψ_{n-M}(-1 - S_M)]| ≤ B (ε' (p + q) + 2 P(I_1 = 1, |S_M| > r) + 2 q P(|S_M| > r)). At an incompatible endpoint the weight Ψ_{n-M}(-1 - S_M) vanishes.

Lemma lem:1 and Proposition prop:b3bis

theorem PoissonDeclumping.Bridge.exists_eventually_mul_abs_integral_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) {ε : ℝ} (hε : 0 < ε) : ∃ (ε' : ℝ), 0 < ε' ∧ ∀ᶠ (n : ℕ) in admissibleSizes μ, ∀ (f : ℕ → ℝ), (∀ (w : ℕ), |f w| ≤ 1) → ∀ (κ : ℝ), |κ| ≤ 1 → (∀ (x : ℤ), |↑x| ≤ √(a (M n) * a n) → walkProb μ (↑(n - M n)) (-1 - x) ≠ 0 → |endpointMean μ (G (k n)) (M n) n f x - κ| ≤ ε') → ↑n * |∫ (ω : Fin n → ℤ), ((markSet (G (k n)) (M n)).indicator 1 (List.ofFn ω) - qProb μ (G (k n)) (M n) n) * (endpointMean μ (G (k n)) (M n) n f (List.take (M n) (List.ofFn ω)).sum - κ) ∂Lukasiewicz.bridgeLaw μ n| ≤ ε

The combination step of Lemma lem:1 (source lines 1898–1924): for every ε > 0 there is ε' > 0 such that, eventually along admissible sizes, for every test function ‖f‖_∞ ≤ 1 and every constant |κ| ≤ 1 with |h_n(k) - κ| ≤ ε' at all compatible endpoints |k| ≤ r_n = √(a_{M_n} a_n), n |E[(I_1^{(M_n)} - q_n)(h_n(S_{M_n}) - κ) | S_n = -1]| ≤ ε. The large endpoints are controlled by Lemma lem:pnqn(i) and marginal tightness (correction F6), the small ones by 2 n q_n ε'; only bounded n π_n and the cutoff properties are used.

theorem PoissonDeclumping.Bridge.eventually_lem1 {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in admissibleSizes μ, ∀ (f : ℕ → ℝ), (∀ (w : ℕ), |f w| ≤ 1) → ∀ (k₀ : ℤ), |↑k₀| ≤ √(a (M n) * a n) → walkProb μ (↑(n - M n)) (-1 - k₀) ≠ 0 → ↑n * |∫ (ω : Fin n → ℤ), ((markSet (G (k n)) (M n)).indicator 1 (List.ofFn ω) - qProb μ (G (k n)) (M n) n) * (endpointMean μ (G (k n)) (M n) n f (List.take (M n) (List.ofFn ω)).sum - endpointMean μ (G (k n)) (M n) n f k₀) ∂Lukasiewicz.bridgeLaw μ n| ≤ ε

Lemma lem:1 (source lines 1872–1876, proof 1891–1995), with a compatible base point (correction F2): for every ε > 0, eventually along admissible sizes, for every test function ‖f‖_∞ ≤ 1 and every base point k₀ with |k₀| ≤ r_n = √(a_{M_n} a_n) and Ψ_{n-M_n}(-1-k₀) ≠ 0, with Δ_n(k) = h_n(k) - h_n(k₀), n |E[(I_1^{(M_n)} - q_n) Δ_n(S_{M_n}) | S_n = -1]| ≤ ε. (The paper's base point is k₀ = 0, compatible exactly when d ∣ M_n; in the aperiodic case d = 1 it is always admissible here.)

theorem PoissonDeclumping.Bridge.tendsto_lem1 {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) (f : ℕ → ℕ → ℝ) (hf : ∀ (n w : ℕ), |f n w| ≤ 1) (k₀ : ℕ → ℤ) (hk₀ : ∀ᶠ (n : ℕ) in admissibleSizes μ, |↑(k₀ n)| ≤ √(a (M n) * a n) ∧ walkProb μ (↑(n - M n)) (-1 - k₀ n) ≠ 0) : Filter.Tendsto (fun (n : ℕ) => ↑n * ∫ (ω : Fin n → ℤ), ((markSet (G (k n)) (M n)).indicator 1 (List.ofFn ω) - qProb μ (G (k n)) (M n) n) * (endpointMean μ (G (k n)) (M n) n (f n) (List.take (M n) (List.ofFn ω)).sum - endpointMean μ (G (k n)) (M n) n (f n) (k₀ n)) ∂Lukasiewicz.bridgeLaw μ n) (admissibleSizes μ) (nhds 0)

Lemma lem:1, sequential form: for test functions f_n with ‖f_n‖_∞ ≤ 1 and compatible base points k₀(n) with |k₀(n)| ≤ r_n, n E[(I_1^{(M_n)} - q_n) Δ_n(S_{M_n}) | S_n = -1] → 0 along admissible sizes.

theorem PoissonDeclumping.Bridge.eventually_errorB3_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in admissibleSizes μ, ∀ (f : ℕ → ℝ), (∀ (w : ℕ), |f w| ≤ 1) → errorB3 μ (G (k n)) (M n) n f ≤ ε

Proposition prop:b3bis, uniform form (source lines 1862–1864, proof 1880–1886): for every ε > 0, eventually along admissible sizes, b_3^n(f) ≤ ε for every test function ‖f‖_∞ ≤ 1. This is the form needed after exists_paperTVDist_cyclicSum_le_errorTerms, whose test function depends on n. Proof: cyclic exchangeability and block reduction (errorB3_eq_mul, integral_blockIntegrand_eq) with a compatible base value κ = h_n(k₀) (correction F2; if no compatible endpoint |k₀| ≤ r_n exists, κ = 0 and the small-endpoint part is empty), then exists_eventually_mul_abs_integral_le and eventually_abs_endpointMean_sub_le. Assumption (M) is not needed.

theorem PoissonDeclumping.Bridge.errorB3_nonneg (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) (f : ℕ → ℝ) : 0 ≤ errorB3 μ G M n f

b_3 is nonnegative.

theorem PoissonDeclumping.Bridge.tendsto_errorB3 {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) (f : ℕ → ℕ → ℝ) (hf : ∀ (n w : ℕ), |f n w| ≤ 1) : Filter.Tendsto (fun (n : ℕ) => errorB3 μ (G (k n)) (M n) n (f n)) (admissibleSizes μ) (nhds 0)

Proposition prop:b3bis (source lines 1862–1864): for test functions f_n with ‖f_n‖_∞ ≤ 1, if (n π_n) is bounded then b_3^n → 0 along admissible sizes (periodic offspring laws included, correction F2).