Functions which vanish as distributions vanish as functions

In a finite dimensional normed real vector space endowed with a Borel measure, consider a locally integrable function whose integral against all compactly supported smooth functions vanishes. Then the function is almost everywhere zero. This is proved in ae_eq_zero_of_integral_contDiff_smul_eq_zero.

A version for two functions having the same integral when multiplied by smooth compactly supported functions is also given in ae_eq_of_integral_contDiff_smul_eq.

These are deduced from the same results on finite-dimensional real manifolds, given respectively as ae_eq_zero_of_integral_smooth_smul_eq_zero and ae_eq_of_integral_smooth_smul_eq.

theorem ae_eq_zero_of_integral_smooth_smul_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [MeasurableSpace M] [BorelSpace M] [SigmaCompactSpace M] [T2Space M] {f : M → F} {μ : MeasureTheory.Measure M} (hf : MeasureTheory.LocallyIntegrable f μ) (h : ∀ (g : M → ℝ), Smooth 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.

theorem IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M → F} {μ : MeasureTheory.Measure M} {U : Set M} (hU : IsOpen U) (hSig : IsSigmaCompact U) (hf : MeasureTheory.LocallyIntegrableOn f U μ) (h : ∀ (g : M → ℝ), Smooth I (modelWithCornersSelf ℝ ℝ) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0) : ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0

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

theorem IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [MeasurableSpace M] [BorelSpace M] [SigmaCompactSpace M] [T2Space M] {f : M → F} {μ : MeasureTheory.Measure M} {U : Set M} (hU : IsOpen U) (hf : MeasureTheory.LocallyIntegrableOn f U μ) (h : ∀ (g : M → ℝ), Smooth I (modelWithCornersSelf ℝ ℝ) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0) : ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0

theorem ae_eq_of_integral_smooth_smul_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [MeasurableSpace M] [BorelSpace M] [SigmaCompactSpace M] [T2Space M] {f : M → F} {f' : M → F} {μ : MeasureTheory.Measure M} (hf : MeasureTheory.LocallyIntegrable f μ) (hf' : MeasureTheory.LocallyIntegrable f' μ) (h : ∀ (g : M → ℝ), Smooth 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.

theorem ae_eq_zero_of_integral_contDiff_smul_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {f : E → F} {μ : MeasureTheory.Measure E} (hf : MeasureTheory.LocallyIntegrable f μ) (h : ∀ (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.

theorem ae_eq_of_integral_contDiff_smul_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {f : E → F} {f' : E → F} {μ : MeasureTheory.Measure E} (hf : MeasureTheory.LocallyIntegrable f μ) (hf' : MeasureTheory.LocallyIntegrable f' μ) (h : ∀ (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.

theorem IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {f : E → F} {μ : MeasureTheory.Measure E} {U : Set E} (hU : IsOpen U) (hf : MeasureTheory.LocallyIntegrableOn f U μ) (h : ∀ (g : E → ℝ), ContDiff ℝ ⊤ g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : E), g x • f x ∂μ = 0) : ∀ᵐ (x : E) ∂μ, x ∈ U → f x = 0

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