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 α β)
:
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)
:
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)
:
@[simp]
theorem
ProbabilityTheory.Kernel.comp_id
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : Kernel α β)
:
@[simp]
theorem
ProbabilityTheory.Kernel.id_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : Kernel α β)
:
@[simp]
theorem
ProbabilityTheory.Kernel.swap_swap
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
:
theorem
ProbabilityTheory.Kernel.swap_comp_eq_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{κ : Kernel α (β × γ)}
:
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 : γ → δ)
:
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)
:
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 β (γ × δ))
:
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 β (γ × δ))
: