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.
Main statements #
parallelComp_comp_parallelComp:(η ∥ₖ η') ∘ₖ (κ ∥ₖ κ') = (η ∘ₖ κ) ∥ₖ (η' ∘ₖ κ')
theorem
MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
:
μ.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 κ]
:
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 κ]
:
theorem
ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{κ : Kernel α β}
{α' : Type u_5}
{mα' : MeasurableSpace α'}
[IsSFiniteKernel κ]
{η : Kernel α' γ}
[IsSFiniteKernel η]
{ξ : Kernel γ δ}
[IsSFiniteKernel ξ]
:
theorem
ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{κ : Kernel α β}
{α' : Type u_5}
{mα' : MeasurableSpace α'}
[IsSFiniteKernel κ]
{η : Kernel α' γ}
[IsSFiniteKernel η]
{ξ : Kernel γ δ}
[IsSFiniteKernel ξ]
:
theorem
ProbabilityTheory.Kernel.parallelComp_comp_parallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{α' : Type u_5}
{β' : Type u_6}
{γ' : Type u_7}
{mα' : MeasurableSpace α'}
{mβ' : MeasurableSpace β'}
{mγ' : MeasurableSpace γ'}
[IsSFiniteKernel κ]
{η : Kernel β γ}
[IsSFiniteKernel η]
{κ' : Kernel α' β'}
[IsSFiniteKernel κ']
{η' : Kernel β' γ'}
[IsSFiniteKernel η']
:
theorem
ProbabilityTheory.Kernel.parallelComp_comp_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{β' : Type u_6}
{γ' : Type u_7}
{mβ' : MeasurableSpace β'}
{mγ' : MeasurableSpace γ'}
[IsSFiniteKernel κ]
{η : Kernel β γ}
[IsSFiniteKernel η]
{κ' : Kernel α β'}
[IsSFiniteKernel κ']
{η' : Kernel β' γ'}
[IsSFiniteKernel η']
:
theorem
ProbabilityTheory.Kernel.parallelComp_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel γ δ}
[IsSFiniteKernel η]
:
(Kernel.id.parallelComp κ).comp (η.parallelComp Kernel.id) = (η.parallelComp Kernel.id).comp (Kernel.id.parallelComp κ)
theorem
MeasureTheory.Measure.parallelComp_comp_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel β γ}
[ProbabilityTheory.IsSFiniteKernel η]
: