structure IsMarkovChain {Ω : Type u_1} {S : Type u_2} {m : MeasurableSpace Ω} [MeasurableSpace S] (X : ℕ → Ω → S) (ℱ : MeasureTheory.Filtration ℕ m) (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure Ω) : Prop

IsMarkovChain X ℱ κ μ asserts that the sequence of random variables X : ℕ → Ω → S is a Markov chain with respect to the filtration ℱ with transition probability kernel κ under the measure μ. Concretely it requires that X is ℱ-adapted and that for each n and measurable B ⊆ S,

μ[1_{B} ∘ X (n+1) | ℱ n] = κ (X n ·) B μ-a.e.,

which is the standard form P(X_{n+1} ∈ B | ℱ_n) = κ(X n, B) of the Markov property.

• adapted : MeasureTheory.Adapted ℱ X
• markov_prop (n : ℕ) (B : Set S) : MeasurableSet B → μ[(B.indicator fun (x : S) => 1) ∘ X (n + 1) | ↑ℱ n] =ᵐ[μ] fun (ω : Ω) => ((κ (X n ω)) B).toReal