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.

def ProbabilityTheory.«term_∘ₘ_».«delab_app.MeasureTheory.Measure.bind» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.«term_∘ₘ_» : Lean.TrailingParserDescr

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.

@[simp]

theorem MeasureTheory.Measure.comp_apply_univ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel κ] : (μ.bind ⇑κ) Set.univ = μ Set.univ

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 • ν