Lemmas relating different ways to compose kernels #
This file contains lemmas about the composition of kernels that involve several types of compositions/products.
Main statements #
comp_eq_snd_compProd:η ∘ₖ κ = snd (κ ⊗ₖ prodMkLeft X η)parallelComp_comp_parallelComp:(η ∥ₖ η') ∘ₖ (κ ∥ₖ κ') = (η ∘ₖ κ) ∥ₖ (η' ∘ₖ κ')deterministic_comp_copy: for a deterministic kernel, copying then applying the kernel to the two copies is the same as first applying the kernel then copying. That is, ifκis a deterministic kernel,(κ ∥ₖ κ) ∘ₖ copy X = copy Y ∘ₖ κ.
theorem
ProbabilityTheory.Kernel.comp_eq_snd_compProd
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{mZ : MeasurableSpace Z}
(η : Kernel Y Z)
[IsSFiniteKernel η]
(κ : Kernel X Y)
[IsSFiniteKernel κ]
:
@[simp]
theorem
ProbabilityTheory.Kernel.snd_compProd_prodMkLeft
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{mZ : MeasurableSpace Z}
(κ : Kernel X Y)
(η : Kernel Y Z)
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Kernel.compProd_prodMkLeft_eq_comp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{mZ : MeasurableSpace Z}
(κ : Kernel X Y)
[IsSFiniteKernel κ]
(η : Kernel Y Z)
[IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Kernel.swap_parallelComp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{T : Type u_4}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{mZ : MeasurableSpace Z}
{mT : MeasurableSpace T}
{κ : Kernel X Y}
{η : Kernel Z T}
:
theorem
ProbabilityTheory.Kernel.deterministic_comp_copy
{X : Type u_1}
{Y : Type u_2}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{f : X → Y}
(hf : Measurable f)
:
((deterministic f hf).parallelComp (deterministic f hf)).comp (copy X) = (copy Y).comp (deterministic f hf)
For a deterministic kernel, copying then applying the kernel to the two copies is the same as first applying the kernel then copying.
theorem
ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{T : Type u_4}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{mZ : MeasurableSpace Z}
{mT : MeasurableSpace T}
{κ : Kernel X Y}
{X' : Type u_5}
{mX' : MeasurableSpace X'}
{η : Kernel X' Z}
[IsSFiniteKernel η]
{ξ : Kernel Z T}
[IsSFiniteKernel ξ]
:
theorem
ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelComp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{T : Type u_4}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{mZ : MeasurableSpace Z}
{mT : MeasurableSpace T}
{κ : Kernel X Y}
{X' : Type u_5}
{mX' : MeasurableSpace X'}
{η : Kernel X' Z}
[IsSFiniteKernel η]
{ξ : Kernel Z T}
[IsSFiniteKernel ξ]
:
theorem
ProbabilityTheory.Kernel.parallelComp_comp_parallelComp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{mZ : MeasurableSpace Z}
{κ : Kernel X Y}
{X' : Type u_5}
{Y' : Type u_6}
{Z' : Type u_7}
{mX' : MeasurableSpace X'}
{mY' : MeasurableSpace Y'}
{mZ' : MeasurableSpace Z'}
[IsSFiniteKernel κ]
{η : Kernel Y Z}
[IsSFiniteKernel η]
{κ' : Kernel X' Y'}
[IsSFiniteKernel κ']
{η' : Kernel Y' Z'}
[IsSFiniteKernel η']
:
theorem
ProbabilityTheory.Kernel.parallelComp_comp_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{mZ : MeasurableSpace Z}
{κ : Kernel X Y}
{Y' : Type u_6}
{Z' : Type u_7}
{mY' : MeasurableSpace Y'}
{mZ' : MeasurableSpace Z'}
[IsSFiniteKernel κ]
{η : Kernel Y Z}
[IsSFiniteKernel η]
{κ' : Kernel X Y'}
[IsSFiniteKernel κ']
{η' : Kernel Y' Z'}
[IsSFiniteKernel η']
:
theorem
ProbabilityTheory.Kernel.parallelComp_comm
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{T : Type u_4}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
{mZ : MeasurableSpace Z}
{mT : MeasurableSpace T}
{κ : Kernel X Y}
{η : Kernel Z T}
:
(Kernel.id.parallelComp κ).comp (η.parallelComp Kernel.id) = (η.parallelComp Kernel.id).comp (Kernel.id.parallelComp κ)