Documentation

Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

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] [T2Space M] {f : MF} {μ : MeasureTheory.Measure M} [SigmaCompactSpace M] (hf : MeasureTheory.LocallyIntegrable f μ) (h : ∀ (g : M), Smooth I (modelWithCornersSelf ) gHasCompactSupport 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 : MF} {μ : MeasureTheory.Measure M} {U : Set M} (hU : IsOpen U) (hSig : IsSigmaCompact U) (hf : MeasureTheory.LocallyIntegrableOn f U μ) (h : ∀ (g : M), Smooth I (modelWithCornersSelf ) gHasCompactSupport gtsupport g 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} [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 : MF} {μ : MeasureTheory.Measure M} [SigmaCompactSpace M] {U : Set M} (hU : IsOpen U) (hf : MeasureTheory.LocallyIntegrableOn f U μ) (h : ∀ (g : M), Smooth I (modelWithCornersSelf ) gHasCompactSupport gtsupport g 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} [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 : MF} {f' : MF} {μ : MeasureTheory.Measure M} [SigmaCompactSpace M] (hf : MeasureTheory.LocallyIntegrable f μ) (hf' : MeasureTheory.LocallyIntegrable f' μ) (h : ∀ (g : M), Smooth I (modelWithCornersSelf ) gHasCompactSupport 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 : EF} {μ : MeasureTheory.Measure E} (hf : MeasureTheory.LocallyIntegrable f μ) (h : ∀ (g : E), ContDiff gHasCompactSupport 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 : EF} {f' : EF} {μ : MeasureTheory.Measure E} (hf : MeasureTheory.LocallyIntegrable f μ) (hf' : MeasureTheory.LocallyIntegrable f' μ) (h : ∀ (g : E), ContDiff gHasCompactSupport 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 : EF} {μ : MeasureTheory.Measure E} {U : Set E} (hU : IsOpen U) (hf : MeasureTheory.LocallyIntegrableOn f U μ) (h : ∀ (g : E), ContDiff gHasCompactSupport gtsupport g 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.