English
In sigma-compact spaces with appropriate measurability, if a function has zero integral over all closed sets, it is zero a.e.
Русский
В прострастве с гаммой сигма-компактности и надлежащей измеримости, если функция имеет нулевой интеграл по всем замкнутым множествам, она равна нулю почти повсеместно.
LaTeX
$$$$ f =^{\mathrm{ae}}_{\mu} 0 $$$$
Lean4
/-- If an 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 : Integrable f μ) (h'f : ∀ (s : Set β), IsCompact s → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 :=
by
apply ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero hf (fun s hs ↦ ?_)
let t : ℕ → Set β := fun n ↦ closure (compactCovering β n) ∩ s
suffices H : Tendsto (fun n ↦ ∫ x in t n, f x ∂μ) atTop (𝓝 (∫ x in s, f x ∂μ))
by
have A : ∀ n, ∫ x in t n, f x ∂μ = 0 := fun n ↦ h'f _ ((isCompact_compactCovering β n).closure.inter_right hs)
simp_rw [A, tendsto_const_nhds_iff] at H
exact H.symm
have B : s = ⋃ n, t n := by rw [← Set.iUnion_inter, iUnion_closure_compactCovering, Set.univ_inter]
rw [B]
apply tendsto_setIntegral_of_monotone
· intro n
exact (isClosed_closure.inter hs).measurableSet
· intro m n hmn
simp only [t, Set.le_iff_subset]
gcongr
· exact hf.integrableOn
