Lemmas relating different ways to compose measures and kernels

This file contains lemmas about the composition of measures and kernels that do not fit in any of the other files in this directory, because they involve several types of compositions/products.

theorem ProbabilityTheory.Kernel.prod_prodMkLeft_comp_prod_deterministic {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {β' : Type u_5} {ε : Type u_6} {mβ' : MeasurableSpace β'} {mε : MeasurableSpace ε} (κ : Kernel γ β) [IsSFiniteKernel κ] (η : Kernel ε β') [IsSFiniteKernel η] (ξ : Kernel (β × ε) δ) [IsSFiniteKernel ξ] {f : γ → ε} (hf : Measurable f) : (ξ.prod (prodMkLeft β η)).comp (κ.prod (deterministic f hf)) = (ξ.comp (κ.prod (deterministic f hf))).prod (η.comp (deterministic f hf))

The composition of two product kernels (ξ ×ₖ η') ∘ₖ (κ ×ₖ ζ) is the product of the compositions (ξ ∘ₖ (κ ×ₖ ζ)) ×ₖ (η' ∘ₖ (κ ×ₖ ζ)), if ζ is deterministic (of the form .deterministic f hf) and η' does not depend on the output of κ. That is, η' has the form η.prodMkLeft β for a kernel η.

If κ was deterministic, this would be true even if η.prodMkLeft β was a more general kernel since κ ×ₖ Kernel.deterministic f hf would be deterministic and commute with copying. Here κ is not deterministic, but it is discarded in one branch of the copy.

theorem ProbabilityTheory.Kernel.prod_prodMkRight_comp_deterministic_prod {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {β' : Type u_5} {ε : Type u_6} {mβ' : MeasurableSpace β'} {mε : MeasurableSpace ε} (κ : Kernel γ β) [IsSFiniteKernel κ] (η : Kernel ε β') [IsSFiniteKernel η] (ξ : Kernel (ε × β) δ) [IsSFiniteKernel ξ] {f : γ → ε} (hf : Measurable f) : (ξ.prod (prodMkRight β η)).comp ((deterministic f hf).prod κ) = (ξ.comp ((deterministic f hf).prod κ)).prod (η.comp (deterministic f hf))

The composition of two product kernels (ξ ×ₖ η') ∘ₖ (ζ ×ₖ κ) is the product of the compositions, (ξ ∘ₖ (ζ ×ₖ κ)) ×ₖ (η' ∘ₖ (ζ ×ₖ κ)), if ζ is deterministic (of the form .deterministic f hf) and η' does not depend on the output of κ. That is, η' has the form η.prodMkRight β for a kernel η.

If κ was deterministic, this would be true even if η.prodMkRight β was a more general kernel since Kernel.deterministic f hf ×ₖ κ would be deterministic and commute with copying. Here κ is not deterministic, but it is discarded in one branch of the copy.

theorem MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [SFinite μ] : μ.compProd κ = (μ.bind ⇑(ProbabilityTheory.Kernel.copy α)).bind ⇑(ProbabilityTheory.Kernel.id.parallelComp κ)

theorem MeasureTheory.Measure.prod_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {μ : Measure α} {ν : Measure β} [SFinite ν] {κ : ProbabilityTheory.Kernel β γ} [ProbabilityTheory.IsSFiniteKernel κ] : μ.prod (ν.bind ⇑κ) = (μ.prod ν).bind ⇑(ProbabilityTheory.Kernel.id.parallelComp κ)

theorem MeasureTheory.Measure.prod_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν] {κ : ProbabilityTheory.Kernel α γ} [ProbabilityTheory.IsSFiniteKernel κ] : (μ.bind ⇑κ).prod ν = (μ.prod ν).bind ⇑(κ.parallelComp ProbabilityTheory.Kernel.id)

theorem MeasureTheory.Measure.parallelComp_comp_compProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel β γ} [ProbabilityTheory.IsSFiniteKernel η] : (μ.compProd κ).bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η) = μ.compProd (η.comp κ)

theorem MeasureTheory.Measure.compProd_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {f : β → γ} (hf : Measurable f) : μ.compProd (κ.map f) = map (Prod.map id f) (μ.compProd κ)