Markov decompositions of the Łukasiewicz walk (B05)

Source lines 806–824 (Markov property at ζ in the proof of Corollary cor:cyclicshift) and 1740–1772 (Markov property at a deterministic time and at ζ = j, proof of Lemma lem:pnqn).

Write (X_1, …, X_{m+k}) as the first block (X_1, …, X_m) and the fresh block (X_{m+1}, …, X_{m+k}); these are independent (walkVecLaw_map_split).

• Cyclic.walkVecLaw_zeta_eq_inter: first-tree stopping time and fresh increments after ζ. The event {ζ = m, T(𝐗) ∈ A} depends only on the first m increments, has probability P(𝒯 ∈ A, |𝒯| = m), and is independent of the increments after time m: P(ζ = m, T(𝐗) ∈ A, (X_{m+1}, …, X_{m+k}) ∈ B) = P(𝒯 ∈ A, |𝒯| = m) P((X_1, …, X_k) ∈ B).
• Cyclic.walkVecLaw_firstIndicator_eq: P(I_1^{(M)}(X_1, …, X_n) = 1) = P(G(𝒯) = 1, |𝒯| ≤ M) for M ≤ n (countable decomposition according to ζ = j ≤ M).
• Cyclic.walkVecLaw_firstIndicator_inter_sum: Markov property at the deterministic time M. P(I_1^{(M)} = 1, S_{M+k} = i) = E[I_1^{(M)} Ψ_k(i - S_M)]; with i = -1 and n = M + k this is the formula P(I_1^{(M)} = 1, S_n = -1) = E[I_1^{(M)} Ψ_{n-M}(-1 - S_M)] of source line 1745.

theorem PoissonDeclumping.Cyclic.ofFn_eq_append {m k : ℕ} (ω : Fin (m + k) → ℤ) : List.ofFn ω = (List.ofFn fun (i : Fin m) => ω (Fin.castAdd k i)) ++ List.ofFn fun (j : Fin k) => ω (Fin.natAdd m j)

(x_1, …, x_{m+k}) = (x_1, …, x_m) (x_{m+1}, …, x_{m+k}) as lists.

theorem PoissonDeclumping.Cyclic.zeta_append_eq_some_iff {x y : List ℤ} {m : ℕ} (hx : x.length = m) : Lukasiewicz.zeta (x ++ y) = some m ↔ Lukasiewicz.zeta x = some m

The first passage time at the end of a prefix only depends on the prefix.

theorem PoissonDeclumping.Cyclic.ofSeq_append_of_zeta {x y : List ℤ} (hx : Lukasiewicz.zeta x = some x.length) : PlaneTree.ofSeq (x ++ y) = PlaneTree.ofSeq x

If ζ(𝐱) = |𝐱|, then T(𝐱 𝐲) = T(𝐱).

theorem PoissonDeclumping.Cyclic.walkVecLaw_zeta_eq_length (μ : PMF ℕ) (m : ℕ) (A : Set PlaneTree) : (Lukasiewicz.walkVecLaw μ m) {a : Fin m → ℤ | Lukasiewicz.zeta (List.ofFn a) = some m ∧ ∃ T ∈ A, PlaneTree.ofSeq (List.ofFn a) = some T} = (PlaneTree.bienayme μ) (A ∩ {T : PlaneTree | T.vertexCount = m})

The law of the first excursion: P(ζ(X_1, …, X_m) = m, T(𝐗) ∈ A) = P(𝒯 ∈ A, |𝒯| = m).

theorem PoissonDeclumping.Cyclic.walkVecLaw_zeta_eq_inter (μ : PMF ℕ) (m k : ℕ) (A : Set PlaneTree) (B : Set (Fin k → ℤ)) : (Lukasiewicz.walkVecLaw μ (m + k)) {ω : Fin (m + k) → ℤ | Lukasiewicz.zeta (List.ofFn ω) = some m ∧ (∃ T ∈ A, PlaneTree.ofSeq (List.ofFn ω) = some T) ∧ (fun (j : Fin k) => ω (Fin.natAdd m j)) ∈ B} = (PlaneTree.bienayme μ) (A ∩ {T : PlaneTree | T.vertexCount = m}) * (Lukasiewicz.walkVecLaw μ k) B

B05: first-tree stopping time and fresh increments after ζ. The event {ζ = m, T(𝐗) ∈ A} is determined by (X_1, …, X_m), has probability P(𝒯 ∈ A, |𝒯| = m), and the increments (X_{m+1}, …, X_{m+k}) after time ζ = m are independent of it with the law of (X_1, …, X_k).

theorem PoissonDeclumping.Cyclic.walkVecLaw_zeta_eq_ofSeq_mem (μ : PMF ℕ) {j n : ℕ} (hj : j ≤ n) (A : Set PlaneTree) : (Lukasiewicz.walkVecLaw μ n) {ω : Fin n → ℤ | Lukasiewicz.zeta (List.ofFn ω) = some j ∧ ∃ T ∈ A, PlaneTree.ofSeq (List.ofFn ω) = some T} = (PlaneTree.bienayme μ) (A ∩ {T : PlaneTree | T.vertexCount = j})

P(ζ = j, T(X_1, …, X_n) ∈ A) = P(𝒯 ∈ A, |𝒯| = j) for j ≤ n.

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

p = P(I_1^{(M)}(X_1, …, X_n) = 1) = P(G(𝒯) = 1, |𝒯| ≤ M) for M ≤ n: decompose according to the value j ≤ M of ζ.

theorem PoissonDeclumping.Cyclic.walkVecLaw_firstIndicator_inter_sum (μ : PMF ℕ) (G : PlaneTree → Prop) (M k : ℕ) (i : ℤ) : (Lukasiewicz.walkVecLaw μ (M + k)) {ω : Fin (M + k) → ℤ | firstIndicator G (↑M) (List.ofFn ω) = 1 ∧ ∑ j : Fin (M + k), ω j = i} = ∫⁻ (a : Fin M → ℤ), ↑(firstIndicator G (↑M) (List.ofFn a)) * (walkLaw μ k) {i - ∑ j : Fin M, a j} ∂Lukasiewicz.walkVecLaw μ M

Markov property at the deterministic time M. For n = M + k, P(I_1^{(M)}(X_1, …, X_n) = 1, S_n = i) = E[I_1^{(M)}(X_1, …, X_M) Ψ_{n-M}(i - S_M)].