English
Let U be an open set and f Locally Integrable on U; if ∫ g f = 0 for all smooth compactly supported g on U, then f = 0 a.e. on U.
Русский
Пусть U открыто, f локально интегрируемо на U; если интеграл ∫ g f равен нулю для всех гладких с компактной опорой функций g на U, то f = 0 почти всюду на U.
LaTeX
$$$$\\forall U\\, (\\text{open}),\\ LocallyIntegrableOn(f,U)\\Rightarrow (\\forall g, ContMDiff I 𝓘(ℝ) ∞ g \\Rightarrow HasCompactSupport g \\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
manifold has zero integral when multiplied by any smooth function compactly supported
in `U`, then `f` vanishes almost everywhere in `U`. -/
nonrec theorem ae_eq_zero_of_integral_smooth_smul_eq_zero' {U : Set M} (hU : IsOpen U) (hSig : IsSigmaCompact 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 := by
have meas_U := hU.measurableSet
rw [← ae_restrict_iff' meas_U, ae_restrict_iff_subtype meas_U]
let U : Opens M := ⟨U, hU⟩
change ∀ᵐ (x : U) ∂_, _
haveI : SigmaCompactSpace U := isSigmaCompact_iff_sigmaCompactSpace.mp hSig
refine ae_eq_zero_of_integral_smooth_smul_eq_zero I ?_ fun g g_smth g_supp ↦ ?_
· exact (locallyIntegrable_comap meas_U).mpr hf
specialize
h (Subtype.val.extend g 0) (g_smth.extend_zero g_supp) (g_supp.extend_zero continuous_subtype_val)
((g_supp.tsupport_extend_zero_subset continuous_subtype_val).trans <| Subtype.coe_image_subset _ _)
rw [← setIntegral_eq_integral_of_forall_compl_eq_zero (s := U) fun x hx ↦ ?_] at h
· rw [← integral_subtype_comap] at h
· simp_rw [Subtype.val_injective.extend_apply] at h; exact h
· exact meas_U
rw [Function.extend_apply' _ _ _ (mt _ hx)]
· apply zero_smul
· rintro ⟨x, rfl⟩; exact x.2
