Walk calculus: basic identities, Markov properties and exchangeability

Work package WP1 (remainder) of the bridge plan. Source lines 719–730 (the walk S_k), 777–825 (Ψ_m), 1641–1645 (Markov property at a deterministic time, proof of Lemma lem:error_est), 1720–1728, 1952, 2049 (cyclic exchangeability), 1881 (conditional independence of the blocks given S_{M_n} and S_n, proof of Proposition prop:b3bis), 2058–2073 (two disjoint blocks, proof of Lemma lem:extreme_means).

walkProb μ m x = Ψ_m(x) = P(S_m = x) (Setup/Walk.lean), walkVecLaw μ n is the law of (X_1, …, X_n) (a product measure on Fin n → ℤ), and bridgeLaw μ n its conditioning on S_n = -1. Already available upstream (Cyclic/WalkBridge.lean): walkLaw_eq_map_sum, walkProb_natCast, walkProb_nonneg, walkProb_le_one, walkProb_of_neg, walkProb_neg_one (Dwass), walkProb_neg_one_pos_iff, walkVecLaw_map_split.

Main statements

• walkProb_zero_left, hasSum_walkProb, summable_walkProb: Ψ_0 = δ_0, ∑_x Ψ_m(x) = 1.
• walkProb_add (Chapman–Kolmogorov): Ψ_{m+k}(s) = ∑_x Ψ_m(x) Ψ_k(s - x).
• walkVecLaw_take_inter_sum, walkVecLaw_real_take_inter_sum (Markov property at a deterministic time m ≤ n, for an arbitrary event H on the first m increments): P(H(X_1..X_m), S_n = s) = E[1_{H(X_1..X_m)} Ψ_{n-m}(s - S_m)]; conditional forms cond_real_take, cond_real_take_eq_integral_div (valid for every endpoint s; both sides vanish when Ψ_n(s) = 0).
• map_take_walkVecLaw, map_drop_walkVecLaw, walkVecLaw_take, walkVecLaw_drop: prefix and suffix laws; walkVecLaw_take_inter_drop: independence of the two blocks.
• walkVecLaw_take_drop_sum, cond_take_drop, cond_take_of_take_sum, cond_drop_of_take_sum: conditional independence of (X_1..X_m) and (X_{m+1}..X_n) given S_m = j, S_n = s, with the conditional laws of the two blocks; integral_cond_take_mul_drop: the resulting block reduction E[F(X_1..X_m) G(X_{m+1}..X_n) | S_n = s] = E[F(X_1..X_m) h(S_m) | S_n = s] with h(k) = E[G(X_1..X_{n-m}) | S_{n-m} = s - k], for bounded F, G.
• walkVecLaw_two_blocks, walkVecLaw_two_blocks_inter_sum and walkVecLaw_real_two_blocks_inter_sum: two disjoint blocks (X_1..X_{m₁}), (X_{j+1}..X_{j+m₂}) (m₁ ≤ j, j + m₂ ≤ n) are independent, and P(H₁, H₂, S_n = s) = E[1_{H₁} 1_{H₂} Ψ_{n-m₁-m₂}(s - S_{m₁} - S'_{m₂})].
• map_walkVecLaw_rotate, map_bridgeLaw_rotate, bridgeLaw_rotate, walkVecLaw_rotate: cyclic exchangeability of the walk and of the bridge; take_rotate_eq_take_drop: the first M entries of the i-th cyclic shift are (x_{i+1}, …, x_{i+M}) when i + M ≤ n.
• uniformFringeLaw_real_mul_walkProb: Corollary cor:cyclicshift in multiplied form, P(𝒯^n_{U_n} ∈ A) Ψ_n(-1) = E[1_{𝒯 ∈ A} Ψ_{n-|𝒯|}(0)] for every n.

The paper's sequences are indexed from 1; ours from 0.

Basics

theorem PoissonDeclumping.Bridge.walkProb_zero_left (μ : PMF ℕ) (x : ℤ) : walkProb μ 0 x = if x = 0 then 1 else 0

theorem PoissonDeclumping.Bridge.tsum_walkLaw_singleton (μ : PMF ℕ) (m : ℕ) : ∑' (x : ℤ), (walkLaw μ m) {x} = 1

theorem PoissonDeclumping.Bridge.hasSum_walkProb (μ : PMF ℕ) (m : ℕ) : HasSum (fun (x : ℤ) => walkProb μ (↑m) x) 1

theorem PoissonDeclumping.Bridge.tsum_walkProb (μ : PMF ℕ) (m : ℕ) : ∑' (x : ℤ), walkProb μ (↑m) x = 1

theorem PoissonDeclumping.Bridge.summable_walkProb (μ : PMF ℕ) (m : ℤ) : Summable (walkProb μ m)

Chapman–Kolmogorov

theorem PoissonDeclumping.Bridge.walkLaw_add_eq_map (μ : PMF ℕ) (m k : ℕ) : walkLaw μ (m + k) = MeasureTheory.Measure.map (fun (p : ℤ × ℤ) => p.1 + p.2) ((walkLaw μ m).prod (walkLaw μ k))

theorem PoissonDeclumping.Bridge.walkLaw_add_singleton (μ : PMF ℕ) (m k : ℕ) (s : ℤ) : (walkLaw μ (m + k)) {s} = ∑' (x : ℤ), (walkLaw μ m) {x} * (walkLaw μ k) {s - x}

theorem PoissonDeclumping.Bridge.walkProb_add (μ : PMF ℕ) (m k : ℕ) (s : ℤ) : walkProb μ (↑(m + k)) s = ∑' (x : ℤ), walkProb μ (↑m) x * walkProb μ (↑k) (s - x)

Splitting the increments

theorem PoissonDeclumping.Bridge.walkVecLaw_eq_map_append (μ : PMF ℕ) (m k : ℕ) : Lukasiewicz.walkVecLaw μ (m + k) = MeasureTheory.Measure.map (fun (p : (Fin m → ℤ) × (Fin k → ℤ)) => Fin.append p.1 p.2) ((Lukasiewicz.walkVecLaw μ m).prod (Lukasiewicz.walkVecLaw μ k))

theorem PoissonDeclumping.Bridge.lintegral_walkVecLaw_add (μ : PMF ℕ) (m k : ℕ) (F : (Fin (m + k) → ℤ) → ENNReal) : ∫⁻ (ω : Fin (m + k) → ℤ), F ω ∂Lukasiewicz.walkVecLaw μ (m + k) = ∫⁻ (a : Fin m → ℤ), ∫⁻ (b : Fin k → ℤ), F (Fin.append a b) ∂Lukasiewicz.walkVecLaw μ k ∂Lukasiewicz.walkVecLaw μ m

theorem PoissonDeclumping.Bridge.sum_append {m k : ℕ} (a : Fin m → ℤ) (b : Fin k → ℤ) : ∑ i : Fin (m + k), Fin.append a b i = ∑ i : Fin m, a i + ∑ i : Fin k, b i

theorem PoissonDeclumping.Bridge.take_ofFn_append {m k : ℕ} (a : Fin m → ℤ) (b : Fin k → ℤ) : List.take m (List.ofFn (Fin.append a b)) = List.ofFn a

theorem PoissonDeclumping.Bridge.drop_ofFn_append {m k : ℕ} (a : Fin m → ℤ) (b : Fin k → ℤ) : List.drop m (List.ofFn (Fin.append a b)) = List.ofFn b

Markov property at a deterministic time

theorem PoissonDeclumping.Bridge.walkVecLaw_take_inter_sum (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H : List ℤ → Prop) (s : ℤ) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | H (List.take m (List.ofFn ω)) ∧ ∑ i : Fin n, ω i = s} = ∫⁻ (a : Fin m → ℤ), {a : Fin m → ℤ | H (List.ofFn a)}.indicator (fun (a : Fin m → ℤ) => (walkLaw μ (n - m)) {s - ∑ i : Fin m, a i}) a ∂Lukasiewicz.walkVecLaw μ m

Markov property at the deterministic time m (source lines 1641–1645), measure form: P(H(X_1, …, X_m), S_n = s) = E[1_{H(X_1, …, X_m)} Ψ_{n-m}(s - S_m)].

theorem PoissonDeclumping.Bridge.walkVecLaw_real_take_inter_sum (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H : List ℤ → Prop) (s : ℤ) : (Lukasiewicz.walkVecLaw μ n).real {ω : Fin n → ℤ | H (List.take m (List.ofFn ω)) ∧ ∑ i : Fin n, ω i = s} = ∫ (a : Fin m → ℤ), {a : Fin m → ℤ | H (List.ofFn a)}.indicator 1 a * walkProb μ (↑(n - m)) (s - ∑ i : Fin m, a i) ∂Lukasiewicz.walkVecLaw μ m

Markov property at the deterministic time m, in ℝ (source lines 1641–1645): P(H(X_1, …, X_m), S_n = s) = E[1_{H(X_1, …, X_m)} Ψ_{n-m}(s - S_m)] for m ≤ n.

theorem PoissonDeclumping.Bridge.cond_real_take (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H : List ℤ → Prop) (s : ℤ) : (Lukasiewicz.walkVecLaw μ n)[|{ω : Fin n → ℤ | ∑ i : Fin n, ω i = s}].real {ω : Fin n → ℤ | H (List.take m (List.ofFn ω))} = (walkProb μ (↑n) s)⁻¹ * ∫ (a : Fin m → ℤ), {a : Fin m → ℤ | H (List.ofFn a)}.indicator 1 a * walkProb μ (↑(n - m)) (s - ∑ i : Fin m, a i) ∂Lukasiewicz.walkVecLaw μ m

Markov property at the deterministic time m, conditional form (source line 1641): P(H(X_1, …, X_m) | S_n = s) = Ψ_n(s)⁻¹ E[1_{H(X_1, …, X_m)} Ψ_{n-m}(s - S_m)]. It holds for every endpoint s: if Ψ_n(s) = 0 both sides vanish.

theorem PoissonDeclumping.Bridge.cond_real_take_eq_integral_div (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H : List ℤ → Prop) (s : ℤ) : (Lukasiewicz.walkVecLaw μ n)[|{ω : Fin n → ℤ | ∑ i : Fin n, ω i = s}].real {ω : Fin n → ℤ | H (List.take m (List.ofFn ω))} = ∫ (a : Fin m → ℤ), {a : Fin m → ℤ | H (List.ofFn a)}.indicator 1 a * (walkProb μ (↑(n - m)) (s - ∑ i : Fin m, a i) / walkProb μ (↑n) s) ∂Lukasiewicz.walkVecLaw μ m

The paper's form of cond_real_take: E[H(X_1, …, X_m) | S_n = s] = E[H(X_1, …, X_m) Ψ_{n-m}(s - S_m) / Ψ_n(s)] (source line 1641).

Prefix and suffix laws

theorem PoissonDeclumping.Bridge.map_take_walkVecLaw (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) : MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Lukasiewicz.toVec m (List.take m (List.ofFn ω))) (Lukasiewicz.walkVecLaw μ n) = Lukasiewicz.walkVecLaw μ m

The law of the first m increments (X_1, …, X_m) of (X_1, …, X_n), m ≤ n.

theorem PoissonDeclumping.Bridge.map_drop_walkVecLaw (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) : MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Lukasiewicz.toVec (n - m) (List.drop m (List.ofFn ω))) (Lukasiewicz.walkVecLaw μ n) = Lukasiewicz.walkVecLaw μ (n - m)

Suffix law. The increments (X_{m+1}, …, X_n) after a deterministic time m ≤ n have the law of (X_1, …, X_{n-m}).

theorem PoissonDeclumping.Bridge.walkVecLaw_drop (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (K : List ℤ → Prop) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | K (List.drop m (List.ofFn ω))} = (Lukasiewicz.walkVecLaw μ (n - m)) {b : Fin (n - m) → ℤ | K (List.ofFn b)}

Suffix law, event form: P(K(X_{m+1}, …, X_n)) = P(K(X_1, …, X_{n-m})).

theorem PoissonDeclumping.Bridge.walkVecLaw_take (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H : List ℤ → Prop) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | H (List.take m (List.ofFn ω))} = (Lukasiewicz.walkVecLaw μ m) {a : Fin m → ℤ | H (List.ofFn a)}

Prefix law, event form: P(H(X_1, …, X_m)) = P(H(X_1, …, X_m)) computed in length n ≥ m.

Cyclic exchangeability

theorem PoissonDeclumping.Bridge.toVec_rotate_ofFn {n : ℕ} (ω : Fin n → ℤ) (i : ℕ) : Lukasiewicz.toVec n ((List.ofFn ω).rotate i) = ω ∘ ⇑(finRotate n ^ i)

toVec n (x.rotate i) is the coordinate permutation ω ∘ (finRotate n)^i.

theorem PoissonDeclumping.Bridge.map_walkVecLaw_rotate (μ : PMF ℕ) (n i : ℕ) : MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Lukasiewicz.toVec n ((List.ofFn ω).rotate i)) (Lukasiewicz.walkVecLaw μ n) = Lukasiewicz.walkVecLaw μ n

Cyclic exchangeability of the walk ((X_1, …, X_n) is invariant under cyclic shifts).

theorem PoissonDeclumping.Bridge.map_bridgeLaw_rotate (μ : PMF ℕ) (n i : ℕ) : MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Lukasiewicz.toVec n ((List.ofFn ω).rotate i)) (Lukasiewicz.bridgeLaw μ n) = Lukasiewicz.bridgeLaw μ n

Cyclic exchangeability of the bridge (source lines 1720, 1728, 1952, 2049): (X_{i+1}, …, X_n, X_1, …, X_i) under P(· | S_n = -1) has the law of (X_1, …, X_n) under P(· | S_n = -1).

theorem PoissonDeclumping.Bridge.bridgeLaw_rotate (μ : PMF ℕ) (n i : ℕ) (P : List ℤ → Prop) : (Lukasiewicz.bridgeLaw μ n) {ω : Fin n → ℤ | P ((List.ofFn ω).rotate i)} = (Lukasiewicz.bridgeLaw μ n) {ω : Fin n → ℤ | P (List.ofFn ω)}

Cyclic exchangeability of the bridge, event form.

theorem PoissonDeclumping.Bridge.walkVecLaw_rotate (μ : PMF ℕ) (n i : ℕ) (P : List ℤ → Prop) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | P ((List.ofFn ω).rotate i)} = (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | P (List.ofFn ω)}

Cyclic exchangeability of the walk, event form.

theorem PoissonDeclumping.Bridge.take_rotate_eq_take_drop {α : Type u_1} {x : List α} {i M : ℕ} (h : i + M ≤ x.length) : List.take M (x.rotate i) = List.take M (List.drop i x)

Before the wrap-around, the first M entries of a cyclic shift are a contiguous block: (x_{i+1}, …, x_{i+M}).

Independent blocks, conditionally on the sums (source line 1881)

theorem PoissonDeclumping.Bridge.walkVecLaw_take_drop_sum (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H K : List ℤ → Prop) (j s : ℤ) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | H (List.take m (List.ofFn ω)) ∧ K (List.drop m (List.ofFn ω)) ∧ (List.take m (List.ofFn ω)).sum = j ∧ ∑ i : Fin n, ω i = s} = (Lukasiewicz.walkVecLaw μ m) {a : Fin m → ℤ | H (List.ofFn a) ∧ ∑ i : Fin m, a i = j} * (Lukasiewicz.walkVecLaw μ (n - m)) {b : Fin (n - m) → ℤ | K (List.ofFn b) ∧ ∑ i : Fin (n - m), b i = s - j}

The two blocks (X_1, …, X_m) and (X_{m+1}, …, X_n) are independent, also jointly with their sums: P(H(X_1..X_m), K(X_{m+1}..X_n), S_m = j, S_n = s) = P(H(X_1..X_m), S_m = j) P(K(X_1..X_{n-m}), S_{n-m} = s - j).

theorem PoissonDeclumping.Bridge.walkVecLaw_take_sum_sum (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (j s : ℤ) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | (List.take m (List.ofFn ω)).sum = j ∧ ∑ i : Fin n, ω i = s} = (walkLaw μ m) {j} * (walkLaw μ (n - m)) {s - j}

P(S_m = j, S_n = s) = Ψ_m(j) Ψ_{n-m}(s - j), in ℝ≥0∞.

theorem PoissonDeclumping.Bridge.cond_take_drop (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H K : List ℤ → Prop) (j s : ℤ) : (Lukasiewicz.walkVecLaw μ n)[{ω : Fin n → ℤ | H (List.take m (List.ofFn ω)) ∧ K (List.drop m (List.ofFn ω))} | {ω : Fin n → ℤ | (List.take m (List.ofFn ω)).sum = j ∧ ∑ i : Fin n, ω i = s}] = (Lukasiewicz.walkVecLaw μ m)[{a : Fin m → ℤ | H (List.ofFn a)} | {a : Fin m → ℤ | ∑ i : Fin m, a i = j}] * (Lukasiewicz.walkVecLaw μ (n - m))[{b : Fin (n - m) → ℤ | K (List.ofFn b)} | {b : Fin (n - m) → ℤ | ∑ i : Fin (n - m), b i = s - j}]

Conditional independence of the blocks given S_m and S_n (source line 1881): under P(· | S_m = j, S_n = s), the blocks (X_1, …, X_m) and (X_{m+1}, …, X_n) are independent, with the laws of (X_1, …, X_m) given S_m = j and of (X_1, …, X_{n-m}) given S_{n-m} = s - j. (All three conditional laws are 0 when the conditioning event is null.)

theorem PoissonDeclumping.Bridge.cond_take_of_take_sum (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H : List ℤ → Prop) (j s : ℤ) (hs : (walkLaw μ (n - m)) {s - j} ≠ 0) : (Lukasiewicz.walkVecLaw μ n)[{ω : Fin n → ℤ | H (List.take m (List.ofFn ω))} | {ω : Fin n → ℤ | (List.take m (List.ofFn ω)).sum = j ∧ ∑ i : Fin n, ω i = s}] = (Lukasiewicz.walkVecLaw μ m)[{a : Fin m → ℤ | H (List.ofFn a)} | {a : Fin m → ℤ | ∑ i : Fin m, a i = j}]

Under P(· | S_m = j, S_n = s), the first block has the law of (X_1, …, X_m) given S_m = j.

theorem PoissonDeclumping.Bridge.cond_drop_of_take_sum (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (K : List ℤ → Prop) (j s : ℤ) (hj : (walkLaw μ m) {j} ≠ 0) : (Lukasiewicz.walkVecLaw μ n)[{ω : Fin n → ℤ | K (List.drop m (List.ofFn ω))} | {ω : Fin n → ℤ | (List.take m (List.ofFn ω)).sum = j ∧ ∑ i : Fin n, ω i = s}] = (Lukasiewicz.walkVecLaw μ (n - m))[{b : Fin (n - m) → ℤ | K (List.ofFn b)} | {b : Fin (n - m) → ℤ | ∑ i : Fin (n - m), b i = s - j}]

Under P(· | S_m = j, S_n = s), the second block has the law of (X_1, …, X_{n-m}) given S_{n-m} = s - j.

Integrals of bounded functions of the blocks

theorem PoissonDeclumping.Bridge.abs_indicator_le_of_abs_le {α : Type u_1} {s : Set α} {f : α → ℝ} {C : ℝ} (hf : ∀ (x : α), |f x| ≤ C) (x : α) : |s.indicator f x| ≤ C

theorem PoissonDeclumping.Bridge.integral_walkVecLaw_add (μ : PMF ℕ) (m k : ℕ) (Φ : (Fin (m + k) → ℤ) → ℝ) {C : ℝ} (hΦ : ∀ (ω : Fin (m + k) → ℤ), |Φ ω| ≤ C) : ∫ (ω : Fin (m + k) → ℤ), Φ ω ∂Lukasiewicz.walkVecLaw μ (m + k) = ∫ (a : Fin m → ℤ), ∫ (b : Fin k → ℤ), Φ (Fin.append a b) ∂Lukasiewicz.walkVecLaw μ k ∂Lukasiewicz.walkVecLaw μ m

Fubini for bounded functions of (X_1, …, X_{m+k}).

theorem PoissonDeclumping.Bridge.integral_indicator_sum_eq (μ : PMF ℕ) (k : ℕ) (G : (Fin k → ℤ) → ℝ) (t : ℤ) : ∫ (b : Fin k → ℤ), {b : Fin k → ℤ | ∑ i : Fin k, b i = t}.indicator G b ∂Lukasiewicz.walkVecLaw μ k = walkProb μ (↑k) t * ∫ (b : Fin k → ℤ), G b ∂(Lukasiewicz.walkVecLaw μ k)[|{b : Fin k → ℤ | ∑ i : Fin k, b i = t}]

E[G(X_1, …, X_k); S_k = t] = Ψ_k(t) E[G(X_1, …, X_k) | S_k = t] (both sides vanish if Ψ_k(t) = 0).

theorem PoissonDeclumping.Bridge.integral_cond_eq {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) {S : Set Ω} (hS : MeasurableSet S) (f : Ω → ℝ) : ∫ (x : Ω), f x ∂P[|S] = (P.real S)⁻¹ * ∫ (x : Ω), S.indicator f x ∂P

∫ f d P(· | S) = P(S)⁻¹ ∫ 1_S f dP, in ℝ.

theorem PoissonDeclumping.Bridge.integral_cond_take_mul_drop (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (s : ℤ) (F G : List ℤ → ℝ) {CF CG : ℝ} (hF : ∀ (x : List ℤ), |F x| ≤ CF) (hG : ∀ (x : List ℤ), |G x| ≤ CG) : ∫ (ω : Fin n → ℤ), F (List.take m (List.ofFn ω)) * G (List.drop m (List.ofFn ω)) ∂(Lukasiewicz.walkVecLaw μ n)[|{ω : Fin n → ℤ | ∑ i : Fin n, ω i = s}] = ∫ (ω : Fin n → ℤ), F (List.take m (List.ofFn ω)) * ∫ (b : Fin (n - m) → ℤ), G (List.ofFn b) ∂(Lukasiewicz.walkVecLaw μ (n - m))[|{b : Fin (n - m) → ℤ | ∑ i : Fin (n - m), b i = s - (List.take m (List.ofFn ω)).sum}] ∂(Lukasiewicz.walkVecLaw μ n)[|{ω : Fin n → ℤ | ∑ i : Fin n, ω i = s}]

Block reduction under the endpoint conditioning (the computation of source line 1881): for bounded F, G and m ≤ n, E[F(X_1..X_m) G(X_{m+1}..X_n) | S_n = s] = E[F(X_1..X_m) h(S_m) | S_n = s], where h(k) = E[G(X_1..X_{n-m}) | S_{n-m} = s - k].

Two disjoint blocks (plan WP1.5, source lines 2058–2073)

theorem PoissonDeclumping.Bridge.walkVecLaw_take_inter_drop (μ : PMF ℕ) {m n : ℕ} (hmn : m ≤ n) (H K : List ℤ → Prop) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | H (List.take m (List.ofFn ω)) ∧ K (List.drop m (List.ofFn ω))} = (Lukasiewicz.walkVecLaw μ m) {a : Fin m → ℤ | H (List.ofFn a)} * (Lukasiewicz.walkVecLaw μ (n - m)) {b : Fin (n - m) → ℤ | K (List.ofFn b)}

Independence of a prefix block and the following increments: P(H(X_1..X_m), K(X_{m+1}..X_n)) = P(H(X_1..X_m)) P(K(X_1..X_{n-m})).

theorem PoissonDeclumping.Bridge.walkVecLaw_two_blocks (μ : PMF ℕ) {m₁ j m₂ n : ℕ} (hj : m₁ ≤ j) (hn : j + m₂ ≤ n) (H₁ H₂ : List ℤ → Prop) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | H₁ (List.take m₁ (List.ofFn ω)) ∧ H₂ (List.take m₂ (List.drop j (List.ofFn ω)))} = (Lukasiewicz.walkVecLaw μ m₁) {a : Fin m₁ → ℤ | H₁ (List.ofFn a)} * (Lukasiewicz.walkVecLaw μ m₂) {c : Fin m₂ → ℤ | H₂ (List.ofFn c)}

Independence of two disjoint blocks (source lines 2058, 2073): for m₁ ≤ j and j + m₂ ≤ n, P(H₁(X_1..X_{m₁}), H₂(X_{j+1}..X_{j+m₂})) = P(H₁(X_1..X_{m₁})) P(H₂(X_1..X_{m₂})).

theorem PoissonDeclumping.Bridge.ofFn_append_append_append {a₁ a₂ a₃ a₄ : ℕ} (a : Fin a₁ → ℤ) (b : Fin a₂ → ℤ) (c : Fin a₃ → ℤ) (d : Fin a₄ → ℤ) : List.ofFn (Fin.append (Fin.append (Fin.append a b) c) d) = List.ofFn a ++ List.ofFn b ++ (List.ofFn c ++ List.ofFn d)

theorem PoissonDeclumping.Bridge.walkVecLaw_two_blocks_inter_sum (μ : PMF ℕ) {m₁ j m₂ n : ℕ} (hj : m₁ ≤ j) (hn : j + m₂ ≤ n) (H₁ H₂ : List ℤ → Prop) (s : ℤ) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | H₁ (List.take m₁ (List.ofFn ω)) ∧ H₂ (List.take m₂ (List.drop j (List.ofFn ω))) ∧ ∑ i : Fin n, ω i = s} = ∫⁻ (a : Fin m₁ → ℤ), ∫⁻ (c : Fin m₂ → ℤ), {a : Fin m₁ → ℤ | H₁ (List.ofFn a)}.indicator (fun (a : Fin m₁ → ℤ) => {c : Fin m₂ → ℤ | H₂ (List.ofFn c)}.indicator (fun (c : Fin m₂ → ℤ) => (walkLaw μ (n - m₁ - m₂)) {s - ∑ i : Fin m₁, a i - ∑ i : Fin m₂, c i}) c) a ∂Lukasiewicz.walkVecLaw μ m₂ ∂Lukasiewicz.walkVecLaw μ m₁

Markov property for two disjoint blocks (plan WP1.5; source lines 2058–2065): for m₁ ≤ j and j + m₂ ≤ n, P(H₁(X_1..X_{m₁}), H₂(X_{j+1}..X_{j+m₂}), S_n = s) = E[1_{H₁(X)} 1_{H₂(X')} Ψ_{n-m₁-m₂}(s - S_{m₁} - S'_{m₂})], with X, X' independent copies of the increments (the remaining n - m₁ - m₂ increments form a fresh walk).

theorem PoissonDeclumping.Bridge.walkVecLaw_real_two_blocks_inter_sum (μ : PMF ℕ) {m₁ j m₂ n : ℕ} (hj : m₁ ≤ j) (hn : j + m₂ ≤ n) (H₁ H₂ : List ℤ → Prop) (s : ℤ) : (Lukasiewicz.walkVecLaw μ n).real {ω : Fin n → ℤ | H₁ (List.take m₁ (List.ofFn ω)) ∧ H₂ (List.take m₂ (List.drop j (List.ofFn ω))) ∧ ∑ i : Fin n, ω i = s} = ∫ (a : Fin m₁ → ℤ), ∫ (c : Fin m₂ → ℤ), {a : Fin m₁ → ℤ | H₁ (List.ofFn a)}.indicator 1 a * {c : Fin m₂ → ℤ | H₂ (List.ofFn c)}.indicator 1 c * walkProb μ (↑(n - m₁ - m₂)) (s - ∑ i : Fin m₁, a i - ∑ i : Fin m₂, c i) ∂Lukasiewicz.walkVecLaw μ m₂ ∂Lukasiewicz.walkVecLaw μ m₁

Markov property for two disjoint blocks, in ℝ (plan WP1.5; source lines 2058–2065): for m₁ ≤ j and j + m₂ ≤ n, P(H₁(X_1..X_{m₁}), H₂(X_{j+1}..X_{j+m₂}), S_n = s) = E[1_{H₁(X)} 1_{H₂(X')} Ψ_{n-m₁-m₂}(s - S_{m₁} - S'_{m₂})] for independent copies X, X'.

Corollary cor:cyclicshift in multiplied form (plan WP1.8)

theorem PoissonDeclumping.Bridge.uniformFringeLaw_real_mul_walkProb (μ : PMF ℕ) (n : ℕ) (A : Set PlaneTree) : (uniformFringeLaw μ n).real A * walkProb μ (↑n) (-1) = ∫ (T : PlaneTree), A.indicator (fun (T : PlaneTree) => walkProb μ (↑n - ↑T.vertexCount) 0) T ∂PlaneTree.bienayme μ

Corollary cor:cyclicshift, multiplied form (source lines 783–824), valid for every n (both sides vanish at inadmissible n): P(𝒯^n_{U_n} ∈ A) Ψ_n(-1) = E[1_{𝒯 ∈ A} Ψ_{n-|𝒯|}(0)].