English
For sigma-compact β with Borel structure, if f is integrable and its integral on every compact set is zero, then f=0 a.e.
Русский
Для пространства β с сигма-компактностью и бореловской структурой, если f интегрируема и интеграл по каждому компактному множеству равен нулю, то f равно нулю почти повсеместно.
LaTeX
$$$$ f =^{\mathrm{ae}}_{\mu} 0 $$$$
Lean4
/-- If a locally integrable function has zero integral on all compact sets in a sigma-compact space,
then it is zero almost everywhere. -/
theorem ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero' [SigmaCompactSpace β] [R1Space β] {μ : Measure β}
{f : β → E} (hf : LocallyIntegrable f μ) (h'f : ∀ (s : Set β), IsCompact s → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 :=
by
rw [← μ.restrict_univ, ← iUnion_closure_compactCovering]
apply (ae_restrict_iUnion_iff _ _).2 (fun n ↦ ?_)
apply ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero
· exact hf.integrableOn_isCompact (isCompact_compactCovering β n).closure
· intro s hs
rw [Measure.restrict_restrict' measurableSet_closure]
exact h'f _ (hs.inter_right isClosed_closure)
