integrable_dirac — Mathlib

English

If a is a point and ‖f a‖ is finite, then f is Integrable with respect to dirac at a, provided f is measurable.

Русский

Если a — точка и ‖f(a)‖ конечна, то f интегрируема по dirac в a, при условии, что f измерима.

LaTeX

$$Integrable f (dirac a) under measurability and finiteness at a.$$

Lean4

/-- In a measurable space with measurable singletons, every function is integrable with respect to
a Dirac measure.
See `integrable_dirac'` for a version which requires `f` to be strongly measurable but does not
need singletons to be measurable. -/
@[fun_prop]
theorem integrable_dirac [MeasurableSingletonClass α] {a : α} {f : α → ε} (hfa : ‖f a‖ₑ < ∞) :
    Integrable f (Measure.dirac a) :=
  ⟨aestronglyMeasurable_dirac, by simpa [HasFiniteIntegral]⟩

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