Marginals of a joint pushed through a parallel composition #
Pushing a product measure through η ∥ₖ η' pushes each factor through its kernel. Pushing a
joint measure on α × β through Kernel.id ∥ₖ η keeps the first marginal and composes the
second with η. The joint is
disintegrated as ρ.fst ⊗ₘ ρ.condKernel. [UPSTREAM] candidate for
Mathlib/Probability/Kernel/Composition/Lemmas.lean.
theorem
MeasureTheory.Measure.parallelComp_comp_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
(η : ProbabilityTheory.Kernel α γ)
[ProbabilityTheory.IsSFiniteKernel η]
(η' : ProbabilityTheory.Kernel β δ)
[ProbabilityTheory.IsSFiniteKernel η']
(μ : Measure α)
[SFinite μ]
(ν : Measure β)
[SFinite ν]
:
(μ.prod ν).bind ⇑(η.parallelComp η') = (μ.bind ⇑η).prod (ν.bind ⇑η')
Pushing a product measure through a parallel composition pushes each factor through its kernel: Fubini for the Giry monad.
theorem
MeasureTheory.Measure.parallelComp_id_comp_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsMarkovKernel η]
(μ : Measure α)
[SFinite μ]
(ν : Measure β)
[SFinite ν]
:
(μ.prod ν).bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η) = μ.prod (ν.bind ⇑η)
theorem
MeasureTheory.Measure.fst_parallelComp_id_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsMarkovKernel η]
[StandardBorelSpace β]
[Nonempty β]
(ρ : Measure (α × β))
[IsFiniteMeasure ρ]
:
(ρ.bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η)).fst = ρ.fst
theorem
MeasureTheory.Measure.snd_parallelComp_id_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsMarkovKernel η]
[StandardBorelSpace β]
[Nonempty β]
(ρ : Measure (α × β))
[IsFiniteMeasure ρ]
:
(ρ.bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η)).snd = ρ.snd.bind ⇑η