Theorems · Theorem · measure theory

MeasureTheory.integrable_dirac

∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  [MeasurableSingletonClass α] {a : α} {f : α → ε},
  ‖f a‖ₑ < ⊤ → MeasureTheory.Integrable f (MeasureTheory.Measure.dirac a)

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.

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

3 results in Mathlib

Foundations

Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceContinuousENormMeasurableSingletonClass