Theorems · Theorem · functional analysis

ae_eq_zero_of_integral_contMDiff_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] {H : Type u_3}
  [inst_6 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [IsManifold I (↑⊤) M] [inst_10 : MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M → F}
  {μ : MeasureTheory.Measure M} [SigmaCompactSpace M],
  MeasureTheory.LocallyIntegrable f μ →
    (∀ (g : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0) →
      ∀ᵐ (x : M) ∂μ, f x = 0

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

Defined in

Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceCompleteSpaceTopologicalSpaceTopologicalSpaceChartedSpaceIsManifoldMeasurableSpaceBorelSpaceT2SpaceSigmaCompactSpace