English
In an open subset of a vector space, if locally integrable f satisfies ∫ g f = 0 for all smooth compactly supported g in that open set, then f vanishes almost everywhere in the open set.
Русский
В открытом подмножестве вектора пространство, если f локально интегрируема и для всех гладких компактно поддерживаемых g выполнено ∫ g f = 0, то f = 0 почти всюду в этом открытом множестве.
LaTeX
$$$$\\forall U\\text{ open},\\ LocallyIntegrableOn(f,U)\\Rightarrow (\\forall g, ContMDiff I 𝓘(ℝ) ∞ g \\Rightarrow HasCompactSupport g \\Rightarrow tg g ⊆ U \\Rightarrow \\int g f = 0) \\Rightarrow f = 0 \\text{ a.e. on } U.$$$$
Lean4
theorem ae_eq_zero_of_integral_smooth_smul_eq_zero {U : Set M} (hU : IsOpen U) (hf : LocallyIntegrableOn f U μ)
(h : ∀ g : M → ℝ, ContMDiff I 𝓘(ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U → ∫ x, g x • f x ∂μ = 0) :
∀ᵐ x ∂μ, x ∈ U → f x = 0 :=
haveI := I.locallyCompactSpace
haveI := ChartedSpace.locallyCompactSpace H M
haveI := hU.locallyCompactSpace
haveI := I.secondCountableTopology
haveI := ChartedSpace.secondCountable_of_sigmaCompact H M
hU.ae_eq_zero_of_integral_smooth_smul_eq_zero' _ (isSigmaCompact_iff_sigmaCompactSpace.mpr inferInstance) hf h
