Notation for the composition of a measure and a kernel #
This operation, for which we introduce the notation ∘ₘ, takes μ : Measure α and
κ : Kernel α β and creates κ ∘ₘ μ : Measure β. The integral of a function against κ ∘ₘ μ is
∫⁻ x, f x ∂(κ ∘ₘ μ) = ∫⁻ a, ∫⁻ b, f b ∂(κ a) ∂μ.
This file does not define composition but only introduces notation for
MeasureTheory.Measure.bind μ κ.
Notation #
κ ∘ₘ μ = MeasureTheory.Measure.bind μ κ, forκa kernel.
@[simp]
theorem
MeasureTheory.Measure.comp_apply_univ
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsMarkovKernel κ]
:
theorem
MeasureTheory.Measure.deterministic_comp_eq_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : Measurable f)
:
μ.bind ⇑(ProbabilityTheory.Kernel.deterministic f hf) = map f μ
@[simp]
theorem
MeasureTheory.Measure.id_comp
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
:
μ.bind ⇑ProbabilityTheory.Kernel.id = μ
theorem
MeasureTheory.Measure.swap_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure (α × β)}
:
μ.bind ⇑(ProbabilityTheory.Kernel.swap α β) = map Prod.swap μ
@[simp]
theorem
MeasureTheory.Measure.const_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{ν : Measure β}
:
μ.bind ⇑(ProbabilityTheory.Kernel.const α ν) = μ Set.univ • ν