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: (η ∥ₖ η') ∘ₖ (κ ∥ₖ κ') = (η ∘ₖ κ) ∥ₖ (η' ∘ₖ κ')

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.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 η'] : (η.parallelComp η').comp (κ.prod κ') = (η.comp κ).prod (η'.comp κ')

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} {η : Kernel Z T} [IsSFiniteKernel κ] : (Kernel.id.parallelComp κ).comp (η.parallelComp Kernel.id) = η.parallelComp κ