Composition-related properties of basic deterministic kernels #
@[simp]
theorem
ProbabilityTheory.Kernel.comp_id
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
:
κ.comp ProbabilityTheory.Kernel.id = κ
@[simp]
theorem
ProbabilityTheory.Kernel.id_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
:
ProbabilityTheory.Kernel.id.comp κ = κ
theorem
ProbabilityTheory.Kernel.compProd_prodMkLeft_eq_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsSFiniteKernel η]
:
κ.compProd (ProbabilityTheory.Kernel.prodMkLeft α η) = (ProbabilityTheory.Kernel.id.prod η).comp κ
@[simp]
theorem
ProbabilityTheory.Kernel.comp_discard
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
:
@[simp]
@[simp]
theorem
ProbabilityTheory.Kernel.swap_swap
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
:
(ProbabilityTheory.Kernel.swap α β).comp (ProbabilityTheory.Kernel.swap β α) = ProbabilityTheory.Kernel.id
theorem
ProbabilityTheory.Kernel.swap_comp_eq_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ProbabilityTheory.Kernel α (β × γ)}
:
(ProbabilityTheory.Kernel.swap β γ).comp κ = κ.map Prod.swap