English
Let U be an open set; if f is Locally Integrable on U and ∫ g f = 0 for all smooth compactly supported g on U, then f = 0 a.e. on U.
Русский
Пусть U открыто; если f локально интегрируема на U и для всех гладких с компактной опорой g выполняется ∫ g f = 0, то f = 0 почти всюду на U.
LaTeX
$$$$\\forall U\\text{ open},\\ LocallyIntegrableOn(f,U,μ)\\Rightarrow (\\forall g, ContMDiff I 𝓘(ℝ) ∞ g \\Rightarrow HasCompactSupport g \\Rightarrow tsupport g ⊆ U \\Rightarrow \\int g f = 0) \\Rightarrow f = 0 \\text{ a.e. on } U.$$$$
Lean4
/-- 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`. -/
theorem ae_eq_zero_of_integral_contDiff_smul_eq_zero {U : Set E} (hU : IsOpen U) (hf : LocallyIntegrableOn f U μ)
(h : ∀ (g : E → ℝ), ContDiff ℝ ∞ g → HasCompactSupport g → tsupport g ⊆ U → ∫ x, g x • f x ∂μ = 0) :
∀ᵐ x ∂μ, x ∈ U → f x = 0 :=
hU.ae_eq_zero_of_integral_smooth_smul_eq_zero 𝓘(ℝ, E) hf (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)
