Lemmas about compositions and maps of kernels

This file contains results that use both the composition of kernels and the map of a kernel by a function.

Map and comap are particular cases of composition: they correspond to composition with a deterministic kernel. See deterministic_comp_eq_map and comp_deterministic_eq_comap.

theorem ProbabilityTheory.Kernel.deterministic_comp_eq_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (hf : Measurable f) (κ : Kernel α β) : (deterministic f hf).comp κ = κ.map f

theorem ProbabilityTheory.Kernel.comp_deterministic_eq_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) (hg : Measurable g) : κ.comp (deterministic g hg) = κ.comap g hg

theorem ProbabilityTheory.Kernel.deterministic_comp_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} {g : γ → α} (hf : Measurable f) (hg : Measurable g) : (deterministic g hg).comp (deterministic f hf) = deterministic (g ∘ f) ⋯

@[simp]

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

theorem ProbabilityTheory.Kernel.swap_comp_eq_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : Kernel α (β × γ)} : (swap β γ).comp κ = κ.map Prod.swap

theorem ProbabilityTheory.Kernel.map_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel β γ) (f : γ → δ) : (η.comp κ).map f = (η.map f).comp κ

theorem ProbabilityTheory.Kernel.comp_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel γ δ) {f : β → γ} (hf : Measurable f) : η.comp (κ.map f) = (η.comap f hf).comp κ

theorem ProbabilityTheory.Kernel.fst_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η.comp κ).fst = η.fst.comp κ

theorem ProbabilityTheory.Kernel.snd_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η.comp κ).snd = η.snd.comp κ