Composition of kernels

We define the composition η ∘ₖ κ of kernels κ : Kernel α β and η : Kernel β γ, which is a kernel from α to γ.

Main definitions

• comp (η : Kernel β γ) (κ : Kernel α β) : Kernel α γ: composition of 2 kernels. We define a notation η ∘ₖ κ = comp η κ. ∫⁻ c, g c ∂((η ∘ₖ κ) a) = ∫⁻ b, ∫⁻ c, g c ∂(η b) ∂(κ a)
• The monoid structure on Kernel α α given by kernel composition.

Main statements

• lintegral_comp: Lebesgue integral of a function against a composition of kernels.
• Instances stating that IsMarkovKernel, IsZeroOrMarkovKernel, IsFiniteKernel and IsSFiniteKernel are stable by composition.
• pow_add_apply_eq_lintegral: Chapman-Kolmogorov equations.

Notation

• η ∘ₖ κ = ProbabilityTheory.Kernel.comp η κ

noncomputable def ProbabilityTheory.Kernel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (η : Kernel β γ) (κ : Kernel α β) : Kernel α γ

Composition of two kernels.

Equations

• η.comp κ = { toFun := fun (a : α) => (κ a).bind ⇑η, measurable' := ⋯ }

def ProbabilityTheory.«term_∘ₖ_» : Lean.TrailingParserDescr

Composition of two kernels.

Equations

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

theorem ProbabilityTheory.Kernel.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (η : Kernel β γ) (κ : Kernel α β) (a : α) : (η.comp κ) a = (κ a).bind ⇑η

theorem ProbabilityTheory.Kernel.comp_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (η : Kernel β γ) (κ : Kernel α β) (a : α) {s : Set γ} (hs : MeasurableSet s) : ((η.comp κ) a) s = ∫⁻ (b : β), (η b) s ∂κ a

theorem ProbabilityTheory.Kernel.comp_apply_univ_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel β γ) (a : α) : ((η.comp κ) a) Set.univ ≤ (κ a) Set.univ * η.bound

@[simp]

theorem ProbabilityTheory.Kernel.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) : comp 0 κ = 0

@[simp]

theorem ProbabilityTheory.Kernel.comp_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel β γ) : κ.comp 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.id_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : Kernel.id.comp κ = κ

@[simp]

theorem ProbabilityTheory.Kernel.comp_id {β : Type u_2} {γ : Type u_3} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel β γ) : κ.comp Kernel.id = κ

ae filter of the composition

theorem ProbabilityTheory.Kernel.ae_lt_top_of_comp_ne_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α β} {η : Kernel β γ} {s : Set γ} (a : α) (hs : ((η.comp κ) a) s ≠ ⊤) : ∀ᵐ (b : β) ∂κ a, (η b) s < ⊤

theorem ProbabilityTheory.Kernel.comp_null {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α β} {η : Kernel β γ} {s : Set γ} (a : α) (hs : MeasurableSet s) : ((η.comp κ) a) s = 0 ↔ (fun (y : β) => (η y) s) =ᵐ[κ a] 0

theorem ProbabilityTheory.Kernel.ae_null_of_comp_null {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α β} {η : Kernel β γ} {a : α} {s : Set γ} (h : ((η.comp κ) a) s = 0) : (fun (x : β) => (η x) s) =ᵐ[κ a] 0

theorem ProbabilityTheory.Kernel.ae_ae_of_ae_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α β} {η : Kernel β γ} {a : α} {p : γ → Prop} (h : ∀ᵐ (z : γ) ∂(η.comp κ) a, p z) : ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z

theorem ProbabilityTheory.Kernel.ae_comp_of_ae_ae {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α β} {η : Kernel β γ} {a : α} {p : γ → Prop} (hp : MeasurableSet {z : γ | p z}) (h : ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z) : ∀ᵐ (z : γ) ∂(η.comp κ) a, p z

theorem ProbabilityTheory.Kernel.ae_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α β} {η : Kernel β γ} {a : α} {p : γ → Prop} (hp : MeasurableSet {z : γ | p z}) : (∀ᵐ (z : γ) ∂(η.comp κ) a, p z) ↔ ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z

theorem ProbabilityTheory.Kernel.comp_restrict {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α β} {η : Kernel β γ} {s : Set γ} (hs : MeasurableSet s) : (η.restrict hs).comp κ = (η.comp κ).restrict hs

theorem ProbabilityTheory.Kernel.lintegral_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (η : Kernel β γ) (κ : Kernel α β) (a : α) {g : γ → ENNReal} (hg : Measurable g) : ∫⁻ (c : γ), g c ∂(η.comp κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂η b ∂κ a

theorem ProbabilityTheory.Kernel.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} (ξ : Kernel γ δ) (η : Kernel β γ) (κ : Kernel α β) : (ξ.comp η).comp κ = ξ.comp (η.comp κ)

Composition of kernels is associative.

theorem ProbabilityTheory.Kernel.comp_discard' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : (discard β).comp κ = { toFun := fun (a : α) => (κ a) Set.univ • MeasureTheory.Measure.dirac PUnit.unit, measurable' := ⋯ }

@[simp]

theorem ProbabilityTheory.Kernel.comp_discard {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsMarkovKernel κ] : (discard β).comp κ = discard α

@[simp]

theorem ProbabilityTheory.Kernel.swap_copy {α : Type u_1} {mα : MeasurableSpace α} : (swap α α).comp (copy α) = copy α

theorem ProbabilityTheory.Kernel.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure γ) (κ : Kernel α β) : ⇑((const β μ).comp κ) = fun (a : α) => (κ a) Set.univ • μ

@[simp]

theorem ProbabilityTheory.Kernel.const_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure γ) (κ : Kernel α β) [IsMarkovKernel κ] : (const β μ).comp κ = const α μ

theorem ProbabilityTheory.Kernel.comp_add_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (μ κ : Kernel α β) (η : Kernel β γ) : η.comp (μ + κ) = η.comp μ + η.comp κ

theorem ProbabilityTheory.Kernel.comp_add_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (μ : Kernel α β) (κ η : Kernel β γ) : (κ + η).comp μ = κ.comp μ + η.comp μ

theorem ProbabilityTheory.Kernel.comp_sum_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {ι : Type u_4} [Countable ι] (κ : ι → Kernel α β) (η : Kernel β γ) : η.comp (Kernel.sum κ) = Kernel.sum fun (i : ι) => η.comp (κ i)

theorem ProbabilityTheory.Kernel.comp_sum_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {ι : Type u_4} [Countable ι] (κ : Kernel α β) (η : ι → Kernel β γ) : (Kernel.sum η).comp κ = Kernel.sum fun (i : ι) => (η i).comp κ

theorem ProbabilityTheory.Kernel.copy_comp_apply_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (a : α) {s t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) : (((copy β).comp κ) a) (s ×ˢ t) = (κ a) (s ∩ t)

instance ProbabilityTheory.Kernel.IsMarkovKernel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (η : Kernel β γ) [IsMarkovKernel η] (κ : Kernel α β) [IsMarkovKernel κ] : IsMarkovKernel (η.comp κ)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (η : Kernel β γ) [IsZeroOrMarkovKernel η] : IsZeroOrMarkovKernel (η.comp κ)

instance ProbabilityTheory.Kernel.IsFiniteKernel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (η : Kernel β γ) [IsFiniteKernel η] (κ : Kernel α β) [IsFiniteKernel κ] : IsFiniteKernel (η.comp κ)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (η : Kernel β γ) [IsSFiniteKernel η] (κ : Kernel α β) [IsSFiniteKernel κ] : IsSFiniteKernel (η.comp κ)

@[instance_reducible]

noncomputable instance ProbabilityTheory.Kernel.instMonoid {α : Type u_1} {mα : MeasurableSpace α} : Monoid (Kernel α α)

Equations

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

Chapman-Kolmogorov Equations

theorem ProbabilityTheory.Kernel.pow_add {α : Type u_1} {mα : MeasurableSpace α} (κ : Kernel α α) (m n : ℕ) : κ ^ (m + n) = (κ ^ m).comp (κ ^ n)

The Chapman-Kolmogorov equation, kernel composition version. The n+m-step transition kernel is the composition of the n-step and m-step kernels. Ref. Meyn-Tweedie Theorem 3.4.2, page 68

theorem ProbabilityTheory.Kernel.pow_add_apply_eq_lintegral {α : Type u_1} {mα : MeasurableSpace α} (κ : Kernel α α) (m n : ℕ) (a : α) {s : Set α} (hs : MeasurableSet s) : ((κ ^ (m + n)) a) s = ∫⁻ (b : α), ((κ ^ n) b) s ∂(κ ^ m) a

The Chapman-Kolmogorov equation, integral version.

theorem ProbabilityTheory.Kernel.pow_succ_apply_eq_lintegral {α : Type u_1} {mα : MeasurableSpace α} (κ : Kernel α α) (n : ℕ) (a : α) {s : Set α} (hs : MeasurableSet s) : ((κ ^ (n + 1)) a) s = ∫⁻ (b : α), (κ b) s ∂(κ ^ n) a

A version of the Chapman-Kolmogorov equation useful for paths.