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 κ]
:
η.comp κ = (κ.compProd (prodMkLeft X η)).snd
@[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 η]
:
(κ.compProd (prodMkLeft X η)).snd = η.comp κ
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 η]
:
κ.compProd (prodMkLeft X η) = (Kernel.id.prod η).comp κ
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}
:
(swap Y T).comp (κ.parallelComp η) = (η.parallelComp κ).comp (swap X Z)
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 ξ]
:
(Kernel.id.parallelComp ξ).comp (κ.parallelComp η) = κ.parallelComp (ξ.comp η)
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 ξ]
:
(ξ.parallelComp Kernel.id).comp (η.parallelComp κ) = (ξ.comp η).parallelComp κ
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 η']
:
(η.parallelComp η').comp (κ.parallelComp κ') = (η.comp κ).parallelComp (η'.comp κ')
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 κ)
theorem
ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_id
{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}
[IsSFiniteKernel κ]
(η : Kernel Z T)
:
(Kernel.id.parallelComp κ).comp (η.parallelComp Kernel.id) = η.parallelComp κ