Composition-Product of a measure and a kernel #
This operation, denoted by ⊗ₘ, takes μ : Measure α and κ : kernel α β and creates
μ ⊗ₘ κ : Measure (α × β).
It is defined as ((kernel.const Unit μ) ⊗ₖ (kernel.prodMkLeft Unit κ)) ().
Main definitions #
Measure.compProd: fromμ : Measure αandκ : kernel α β, get aMeasure (α × β).
Notations #
μ ⊗ₘ κ = μ.compProd κ
theorem
ProbabilityTheory.kernel.compProd_preimage_fst
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
{x : α}
{s : Set β}
(hs : MeasurableSet s)
:
((ProbabilityTheory.kernel.compProd κ η) x) (Prod.fst ⁻¹' s) = (κ x) s
theorem
ProbabilityTheory.kernel.compProd_deterministic_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSingletonClass γ]
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α × β → γ}
(hf : Measurable f)
(x : α)
{s : Set (β × γ)}
(hs : MeasurableSet s)
:
((ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.deterministic f hf)) x) s = (κ x) {b : β | (b, f (x, b)) ∈ s}
theorem
MeasureTheory.Measure.comap_swap
{α : Type u_5}
{β : Type u_6}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure (α × β))
:
MeasureTheory.Measure.comap Prod.swap μ = MeasureTheory.Measure.map Prod.swap μ
theorem
ProbabilityTheory.kernel.comap_prod_swap
{δ : Type u_4}
{mδ : MeasurableSpace δ}
{α : Type u_5}
{β : Type u_6}
{γ : Type u_7}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel γ δ))
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
ProbabilityTheory.kernel.comap
(ProbabilityTheory.kernel.prod (ProbabilityTheory.kernel.prodMkRight α η) (ProbabilityTheory.kernel.prodMkLeft γ κ))
Prod.swap ⋯ = ProbabilityTheory.kernel.map
(ProbabilityTheory.kernel.prod (ProbabilityTheory.kernel.prodMkRight γ κ) (ProbabilityTheory.kernel.prodMkLeft α η))
Prod.swap ⋯
theorem
ProbabilityTheory.kernel.map_prod_swap
{α : Type u_5}
{β : Type u_6}
{γ : Type u_7}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel α γ))
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.prod κ η) Prod.swap ⋯ = ProbabilityTheory.kernel.prod η κ