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_contMDiff_smul_eq_zero and ae_eq_of_integral_contMDiff_smul_eq.

source
๐Ÿ“ coverage
theorem ae_eq_zero_of_integral_contMDiff_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] [IsManifold I (โ†‘โŠค) M] [MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M โ†’ F} {ฮผ : MeasureTheory.Measure M} [SigmaCompactSpace M] (hf : MeasureTheory.LocallyIntegrable f ฮผ) (h : โˆ€ (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.

source
๐Ÿ“ coverage
@[deprecated ae_eq_zero_of_integral_contMDiff_smul_eq_zero (since := "2025-12-17")]
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] [IsManifold I (โ†‘โŠค) M] [MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M โ†’ F} {ฮผ : MeasureTheory.Measure M} [SigmaCompactSpace M] (hf : MeasureTheory.LocallyIntegrable f ฮผ) (h : โˆ€ (g : M โ†’ โ„), ContMDiff I (modelWithCornersSelf โ„ โ„) (โ†‘โŠค) g โ†’ HasCompactSupport g โ†’ โˆซ (x : M), g x โ€ข f x โˆ‚ฮผ = 0) :
โˆ€แต (x : M) โˆ‚ฮผ, f x = 0

Alias of ae_eq_zero_of_integral_contMDiff_smul_eq_zero.

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.

source
๐Ÿ“ coverage
instance instBorelSpaceSubtypeMemOpens {M : Type u_4} [TopologicalSpace M] [MeasurableSpace M] [BorelSpace M] (U : TopologicalSpace.Opens M) :
BorelSpace โ†ฅU
source
๐Ÿ“ coverage
theorem IsOpen.ae_eq_zero_of_integral_contMDiff_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] [IsManifold 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 โ†’ โ„), ContMDiff 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.

source
๐Ÿ“ coverage
@[deprecated IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero' (since := "2025-12-17")]
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] [IsManifold 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 โ†’ โ„), ContMDiff I (modelWithCornersSelf โ„ โ„) (โ†‘โŠค) g โ†’ HasCompactSupport g โ†’ tsupport g โŠ† U โ†’ โˆซ (x : M), g x โ€ข f x โˆ‚ฮผ = 0) :
โˆ€แต (x : M) โˆ‚ฮผ, x โˆˆ U โ†’ f x = 0

Alias of IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero'.

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.

source
๐Ÿ“ coverage
theorem IsOpen.ae_eq_zero_of_integral_contMDiff_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] [IsManifold I (โ†‘โŠค) M] [MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M โ†’ F} {ฮผ : MeasureTheory.Measure M} [SigmaCompactSpace M] {U : Set M} (hU : IsOpen U) (hf : MeasureTheory.LocallyIntegrableOn f U ฮผ) (h : โˆ€ (g : M โ†’ โ„), ContMDiff I (modelWithCornersSelf โ„ โ„) (โ†‘โŠค) g โ†’ HasCompactSupport g โ†’ tsupport g โŠ† U โ†’ โˆซ (x : M), g x โ€ข f x โˆ‚ฮผ = 0) :
โˆ€แต (x : M) โˆ‚ฮผ, x โˆˆ U โ†’ f x = 0
source
๐Ÿ“ coverage
@[deprecated IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero (since := "2025-12-17")]
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] [IsManifold I (โ†‘โŠค) M] [MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M โ†’ F} {ฮผ : MeasureTheory.Measure M} [SigmaCompactSpace M] {U : Set M} (hU : IsOpen U) (hf : MeasureTheory.LocallyIntegrableOn f U ฮผ) (h : โˆ€ (g : M โ†’ โ„), ContMDiff I (modelWithCornersSelf โ„ โ„) (โ†‘โŠค) g โ†’ HasCompactSupport g โ†’ tsupport g โŠ† U โ†’ โˆซ (x : M), g x โ€ข f x โˆ‚ฮผ = 0) :
โˆ€แต (x : M) โˆ‚ฮผ, x โˆˆ U โ†’ f x = 0

Alias of IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero.

source
๐Ÿ“ coverage
theorem ae_eq_of_integral_contMDiff_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] [IsManifold I (โ†‘โŠค) M] [MeasurableSpace M] [BorelSpace M] [T2Space M] {f f' : M โ†’ F} {ฮผ : MeasureTheory.Measure M} [SigmaCompactSpace M] (hf : MeasureTheory.LocallyIntegrable f ฮผ) (hf' : MeasureTheory.LocallyIntegrable f' ฮผ) (h : โˆ€ (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.

source
๐Ÿ“ coverage
@[deprecated ae_eq_of_integral_contMDiff_smul_eq (since := "2025-12-17")]
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] [IsManifold I (โ†‘โŠค) M] [MeasurableSpace M] [BorelSpace M] [T2Space M] {f f' : M โ†’ F} {ฮผ : MeasureTheory.Measure M} [SigmaCompactSpace M] (hf : MeasureTheory.LocallyIntegrable f ฮผ) (hf' : MeasureTheory.LocallyIntegrable f' ฮผ) (h : โˆ€ (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

Alias of ae_eq_of_integral_contMDiff_smul_eq.

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.

source
๐Ÿ“ coverage
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.

source
๐Ÿ“ coverage
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 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.

source
๐Ÿ“ coverage
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 vector space has zero integral when multiplied by any smooth function compactly supported in U, then f vanishes almost everywhere in U.