dirac_compProd_apply — Mathlib

English

For a fixed a, the Dirac measure at a combined with κ evaluates on s to κ(a)({b : (a,b) ∈ s}).

Русский

Для фиксированного a.dirac(a) ⊗ κ на s даёт κ(a) ({b : (a,b) ∈ s}).

LaTeX

$$$(\\mathrm{Measure.dirac}\\, a \\otimes_m κ)\\, s = κ a (\\mathrm{Prod.mk} a^{-1}' s)$$$

Lean4

theorem dirac_compProd_apply [MeasurableSingletonClass α] {a : α} [IsSFiniteKernel κ] {s : Set (α × β)}
    (hs : MeasurableSet s) : (Measure.dirac a ⊗ₘ κ) s = κ a (Prod.mk a ⁻¹' s) := by
  rw [compProd_apply hs, lintegral_dirac]

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