Theorems · Theorem · functional analysis

ae_eq_of_integral_contDiff_smul_eq

∀ {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 f' : E → F} {μ : MeasureTheory.Measure E},
  MeasureTheory.LocallyIntegrable f μ →
    MeasureTheory.LocallyIntegrable f' μ →
      (∀ (g : E → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = ∫ (x : E), g x • f' x ∂μ) →
        ∀ᵐ (x : E) ∂μ, f x = f' x

If two locally integrable functions on a finite-dimensional real vector space have the same integral when multiplied by any smooth compactly supported function, then they coincide almost everywhere.

Defined in

Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceCompleteSpaceMeasurableSpaceBorelSpace