boolKernel_comp_measure — Mathlib

English

For μ, ν: measures on α, and π: measure on Bool, π.bind (boolKernel μ ν) equals π{true} ν + π{false} μ.

Русский

Для мер μ, ν на α и π на Bool, π.bind (boolKernel μ ν) = π{true} ν + π{false} μ.

LaTeX

$$$\\pi \\bind (\\text{boolKernel }\\mu \\nu) = \\pi\\{true\\} \\nu + \\pi\\{false\\} \\mu$$$

Lean4

theorem boolKernel_comp_measure (μ ν : Measure α) (π : Measure Bool) :
    Kernel.boolKernel μ ν ∘ₘ π = π { true } • ν + π { false } • μ :=
  by
  ext s hs
  rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
  simp [lintegral_fintype, mul_comm]

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