# 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} [] [] {F : Type u_2} [] [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] [] [] [] {f : MF} {μ : } (hf : ) (h : ∀ (g : M), ∫ (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} [] [] {F : Type u_2} [] [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] [] [] [] {f : MF} {μ : } {U : Set M} (hU : ) (hSig : ) (hf : ) (h : ∀ (g : M), U∫ (x : M), g x f xμ = 0) :
∀ᵐ (x : M) ∂μ, x Uf 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} [] [] {F : Type u_2} [] [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] [] [] [] {f : MF} {μ : } {U : Set M} (hU : ) (hf : ) (h : ∀ (g : M), U∫ (x : M), g x f xμ = 0) :
∀ᵐ (x : M) ∂μ, x Uf x = 0
theorem ae_eq_of_integral_smooth_smul_eq {E : Type u_1} [] [] {F : Type u_2} [] [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] [] [] [] {f : MF} {f' : MF} {μ : } (hf : ) (hf' : ) (h : ∀ (g : M), ∫ (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} [] [] {F : Type u_2} [] [] [] [] {f : EF} {μ : } (hf : ) (h : ∀ (g : E), ∫ (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} [] [] {F : Type u_2} [] [] [] [] {f : EF} {f' : EF} {μ : } (hf : ) (hf' : ) (h : ∀ (g : E), ∫ (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} [] [] {F : Type u_2} [] [] [] [] {f : EF} {μ : } {U : Set E} (hU : ) (hf : ) (h : ∀ (g : E), U∫ (x : E), g x f xμ = 0) :
∀ᵐ (x : E) ∂μ, x Uf 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.