English
On a sigma-compact space, if LocallyIntegrable f and ∀ g smooth with compact support, ∫ g f = ∫ g f', then f = f' a.e.
Русский
На пространстве с синкально-совокупной структурой, если f и f' локально интегрируемы и для всех гладких g с компактной опорой выполняется ∫ g f = ∫ g f', то f = f' a.e.
LaTeX
$$$$\\forall f,f',\\ LocallyIntegrable f,\\ LocallyIntegrable f',\\ (\\forall g, ContMDiff I 𝓘(ℝ) ∞ g \\Rightarrow HasCompactSupport g \\Rightarrow \\int g f = \\int g f') \\Rightarrow f=f' a.e. $$$$
Lean4
/-- 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_of_integral_smooth_smul_eq (hf : LocallyIntegrable f μ) (hf' : LocallyIntegrable f' μ)
(h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ) ∞ g → HasCompactSupport g → ∫ x, g x • f x ∂μ = ∫ x, g x • f' x ∂μ) :
∀ᵐ x ∂μ, f x = f' x :=
by
have : ∀ᵐ x ∂μ, (f - f') x = 0 :=
by
apply ae_eq_zero_of_integral_smooth_smul_eq_zero I (hf.sub hf')
intro g g_diff g_supp
simp only [Pi.sub_apply, smul_sub]
rw [integral_sub, sub_eq_zero]
· exact h g g_diff g_supp
· exact hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
· exact hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
filter_upwards [this] with x hx
simpa [sub_eq_zero] using hx
