def stoppedPathShift {S : Type u_1} (T : (ℕ → S) → ℕ) : (ℕ → S) → ℕ → S

Shift a path ω : ℕ → S by the stopping time T ω: the resulting path at index k is ω (T ω + k).

theorem stoppedPathShift_eq_shiftPath_on_eq {S : Type u_1} (T : (ℕ → S) → ℕ) (n : ℕ) (ω : ℕ → S) (h : T ω = n) : stoppedPathShift T ω = shiftPath n ω

On the event {T ω = n}, the stopping-time shift coincides with the fixed shift by n: stoppedPathShift T ω = shiftPath n ω.

theorem ae_eq_of_ae_eq_restrict_fibers {Ω : Type u_1} {m0 : MeasurableSpace Ω} (T : Ω → ℕ) (μ : MeasureTheory.Measure Ω) (f g : Ω → ℝ) (hT_meas : ∀ (n : ℕ), MeasurableSet {ω : Ω | T ω = n}) (h : ∀ (n : ℕ), f =ᵐ[μ.restrict {ω : Ω | T ω = n}] g) : f =ᵐ[μ] g

If f =ᵐ g on each fiber {T = n} of an ℕ-valued measurable function T, then f =ᵐ g on the whole space.

theorem strong_markov_chain (S : Type u_1) [MeasurableSpace S] [StandardBorelSpace S] [Nonempty S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (T : (ℕ → S) → ℕ) (hT : MeasureTheory.IsStoppingTime (pathFiltration S) fun (ω : ℕ → S) => ↑(T ω)) (Y : ℕ → (ℕ → S) → ℝ) (hY_meas : ∀ (n : ℕ), Measurable (Y n)) (hY_bdd : ∃ (C : ℝ), ∀ (n : ℕ) (ω : ℕ → S), |Y n ω| ≤ C) : have P_μ := MarkovChainPathMeasure S μ κ; P_μ[fun (ω : ℕ → S) => Y (T ω) (stoppedPathShift T ω) | hT.measurableSpace] =ᵐ[P_μ] fun (ω : ℕ → S) => markovExpectation S κ (Y (T ω)) (ω (T ω))

Strong Markov property for Markov chains (Lecture 31). For a Markov chain with initial distribution μ and transition kernel κ on a standard Borel state space S, and a bounded measurable time-indexed functional Y_n, the conditional expectation of Y_T ∘ θ_T given the stopping-time σ-algebra ℱ_T equals E_{X_T} Y_T. This is the discrete-time analogue of E_μ(Y_N ∘ θ_N | ℱ_N) = E_{X_N} Y_N.