Integrable functions vanishing against continuous functions

If an integrable function f on a topological space satisfies ∫ g • f ∂μ = 0 for every bounded continuous real function g, then f = 0 almost everywhere. This is the form in which uniqueness theorems for integral transforms are usually applied: one first shows that the integrals of f against a dense family of test functions vanish (for instance trigonometric polynomials on the circle), extends this by continuity to all bounded continuous functions, and concludes here.

The space only needs indicators of closed sets to be pointwise limits of bounded continuous functions with values in [0, 1] (Mathlib's HasOuterApproxClosed, which holds for every pseudo-metrizable space). Dominated convergence then gives ∫_F f ∂μ = 0 for every closed set F, and Mathlib's MeasureTheory.ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero concludes. No finiteness of μ is needed beyond the integrability of f.

On a locally compact space that need not be metrizable, for instance a locally compact group, there are too few bounded continuous functions approximating indicators pointwise, but for a regular measure the compactly supported continuous functions suffice. Inner regularity approximates a set s of finite measure from inside by a compact set K, outer regularity approximates it from outside by an open set U, and Urysohn's lemma gives a compactly supported continuous function between the indicators of K and U. Its integral against f differs from ∫_s f by at most the integral of ‖f‖ over U \ K, which is small because U \ K has small measure.

Main results

• MeasureTheory.Integrable.ae_eq_zero_of_forall_integral_smul_eq_zero: an integrable function whose integrals against all bounded continuous real functions vanish is zero almost everywhere.
• MeasureTheory.Integrable.ae_eq_of_forall_integral_smul_eq: two integrable functions with the same integrals against all bounded continuous real functions agree almost everywhere.
• MeasureTheory.Integrable.ae_eq_zero_of_forall_integral_hasCompactSupport_smul_eq_zero: for a regular measure on a locally compact space, an integrable function whose integrals against all compactly supported continuous real functions vanish is zero almost everywhere.

theorem MeasureTheory.Integrable.ae_eq_zero_of_forall_integral_smul_eq_zero {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [HasOuterApproxClosed X] {μ : Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : X → E} (hf : Integrable f μ) (h : ∀ (φ : BoundedContinuousFunction X ℝ), ∫ (x : X), φ x • f x ∂μ = 0) : f =ᵐ[μ] 0

Integrable functions are determined by their integrals against bounded continuous functions. If f is integrable and ∫ x, φ x • f x ∂μ = 0 for every bounded continuous φ : X → ℝ, then f = 0 almost everywhere.

theorem MeasureTheory.Integrable.ae_eq_of_forall_integral_smul_eq {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [HasOuterApproxClosed X] {μ : Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : X → E} (hf : Integrable f μ) (hg : Integrable g μ) (h : ∀ (φ : BoundedContinuousFunction X ℝ), ∫ (x : X), φ x • f x ∂μ = ∫ (x : X), φ x • g x ∂μ) : f =ᵐ[μ] g

Two integrable functions with the same integrals against every bounded continuous real function agree almost everywhere.

theorem MeasureTheory.Integrable.ae_eq_zero_of_forall_integral_hasCompactSupport_smul_eq_zero {X : Type u_3} {E : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [LocallyCompactSpace X] [RegularSpace X] {μ : Measure X} [μ.Regular] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : X → E} (hf : Integrable f μ) (h : ∀ (φ : X → ℝ), Continuous φ → HasCompactSupport φ → ∫ (x : X), φ x • f x ∂μ = 0) : f =ᵐ[μ] 0

Integrable functions are determined by their integrals against compactly supported continuous functions for a regular measure on a locally compact space. If f is integrable and ∫ x, φ x • f x ∂μ = 0 for every continuous φ : X → ℝ with compact support, then f = 0 almost everywhere. No metrizability, σ-compactness or σ-finiteness is assumed, and unlike Mathlib's MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported for measures, neither is the Hausdorff property.