Theorems · Theorem · functional analysis

ae_eq_of_integral_contMDiff_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] {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 f' : M → F} {μ : MeasureTheory.Measure M} [SigmaCompactSpace M],
  MeasureTheory.LocallyIntegrable f μ →
    MeasureTheory.LocallyIntegrable f' μ →
      (∀ (g : M → ℝ),
          ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g →
            HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ) →
        ∀ᵐ (x : M) ∂μ, f x = f' x

If two locally integrable functions on a finite-dimensional real manifold 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 302 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceCompleteSpaceTopologicalSpaceTopologicalSpaceChartedSpaceIsManifoldMeasurableSpaceBorelSpaceT2SpaceSigmaCompactSpace