discard_comp — Mathlib

English

If we compose any μ with the discard kernel, the result is μ.univ times the Dirac measure at the unit, i.e., no information is added.

Русский

Композиция меры μ с ядром discard α возвращает μ.univ умноженную на.dirac единицы; информация не добавляется.

LaTeX

$$$\\text{Kernel.discard }\\alpha \\circ_{m} \\mu = \\mu.univ \\cdot \\text{Measure.dirac}(())$$$

Lean4

@[simp]
theorem discard_comp (μ : Measure α) : Kernel.discard α ∘ₘ μ = μ .univ • Measure.dirac () := by ext s hs;
  simp [Measure.bind_apply hs (Kernel.aemeasurable _), mul_comm]

Похожие утверждения