Notation for the compostition 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 μ κ
.
Notations #
κ ∘ₘ μ = MeasureTheory.Measure.bind μ κ
, forκ
a kernel.
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Composition of a measure and a kernel.
Notation for MeasureTheory.Measure.bind
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MeasureTheory.Measure.comp_apply_univ
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsMarkovKernel κ]
: