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:(η ∥ₖ η') ∘ₖ (κ ∥ₖ κ') = (η ∘ₖ κ) ∥ₖ (η' ∘ₖ κ')parallelComp_comp_copy:(κ ∥ₖ η) ∘ₖ (copy α) = κ ×ₖ η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 α = copy β ∘ₖ κ.
theorem
ProbabilityTheory.Kernel.parallelComp_comp_copy
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel α γ)
:
theorem
ProbabilityTheory.Kernel.swap_parallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{κ : Kernel α β}
{η : Kernel γ δ}
:
theorem
ProbabilityTheory.Kernel.deterministic_comp_copy
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
:
((deterministic f hf).parallelComp (deterministic f hf)).comp (copy α) = (copy β).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
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 κ]
:
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 α'}
{η : 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 α'}
{η : 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 α β}
{η : Kernel γ δ}
:
(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 α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel β γ}
[ProbabilityTheory.IsSFiniteKernel η]
: