Kernel utilities #
This file provides helper lemmas for working with kernels.
Main declarations #
comap_parallelComp_comap: the comap of a parallel composition is the parallel composition of the comaps.map_parallelComp_map: the map of a parallel composition is the parallel composition of the maps.
theorem
ProbabilityTheory.Kernel.comap_parallelComp_comap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace ι]
{α₂ : Type u_5}
{γ₂ : Type u_6}
[MeasurableSpace α₂]
[MeasurableSpace γ₂]
(κ : Kernel α β)
(η : Kernel γ ι)
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
{f : α₂ → α}
{g : γ₂ → γ}
(hf : Measurable f)
(hg : Measurable g)
:
(κ.comap f hf).parallelComp (η.comap g hg) = (κ.parallelComp η).comap (fun (a : α₂ × γ₂) => (f a.1, g a.2)) ⋯
theorem
ProbabilityTheory.Kernel.map_parallelComp_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace ι]
{β₂ : Type u_5}
{ι₂ : Type u_6}
[MeasurableSpace β₂]
[MeasurableSpace ι₂]
(κ : Kernel α β)
(η : Kernel γ ι)
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
{f : β → β₂}
{g : ι → ι₂}
(hf : Measurable f)
(hg : Measurable g)
:
instance
ProbabilityTheory.Kernel.instIsSFiniteKernelOfIsDeterministic_eqLift
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(κ : Kernel α β)
[IsDeterministic κ]
: