Theorems · Theorem · functional analysis

ae_eq_zero_of_integral_contDiff_smul_eq_zero

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] [inst_6 : MeasurableSpace E]
  [BorelSpace E] {f : E → F} {μ : MeasureTheory.Measure E},
  MeasureTheory.LocallyIntegrable f μ →
    (∀ (g : E → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = 0) → ∀ᵐ (x : E) ∂μ, f x = 0

If a locally integrable function f on a finite-dimensional real vector space has zero integral when multiplied by any smooth compactly supported function, then f vanishes almost everywhere.

Defined in

Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceCompleteSpaceMeasurableSpaceBorelSpace