Theorems · Theorem · measure theory

MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {β : Type u_3}
  [inst_3 : TopologicalSpace β] [inst_4 : MeasurableSpace β] [BorelSpace β] [SigmaCompactSpace β] [R1Space β]
  {μ : MeasureTheory.Measure β} {f : β → E},
  MeasureTheory.Integrable f μ → (∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0) → f =ᵐ[μ] 0

If an integrable function has zero integral on all compact sets in a sigma-compact space, then it is zero almost everywhere.

Defined in

Mathlib.MeasureTheory.Function.AEEqOfIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceTopologicalSpaceMeasurableSpaceBorelSpaceSigmaCompactSpaceR1Space