# 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`.

source
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
source
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
source
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) ⋯
source
@[simp]
theorem ProbabilityTheory.Kernel.comp_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) :
κ.comp Kernel.id = κ
source
@[simp]
theorem ProbabilityTheory.Kernel.id_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) :
Kernel.id.comp κ = κ
source
@[simp]
theorem ProbabilityTheory.Kernel.swap_swap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
(swap α β).comp (swap β α) = Kernel.id
source
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
source
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 κ
source
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 κ
source
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 κ
source
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 κ