English
If f is integrable and its integral over every closed set is zero, then f is zero almost everywhere.
Русский
Если f интегрируема и интеграл по каждому замкнутому множеству равен нулю, тогда f равно нулю почти повсюду.
LaTeX
$$$$ f =^{\\mathrm{ae}}_{\\mu} 0 $$$$
Lean4
/-- If an integrable function has zero integral on all closed sets, then it is zero
almost everywhere. -/
theorem ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero {μ : Measure β} {f : β → E} (hf : Integrable f μ)
(h'f : ∀ (s : Set β), IsClosed s → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 :=
by
suffices ∀ s, MeasurableSet s → ∫ x in s, f x ∂μ = 0 from
hf.ae_eq_zero_of_forall_setIntegral_eq_zero (fun s hs _ ↦ this s hs)
have A : ∀ (t : Set β), MeasurableSet t → ∫ (x : β) in t, f x ∂μ = 0 → ∫ (x : β) in tᶜ, f x ∂μ = 0 :=
by
intro t t_meas ht
have I : ∫ x, f x ∂μ = 0 := by rw [← setIntegral_univ]; exact h'f _ isClosed_univ
simpa [ht, I] using integral_add_compl t_meas hf
intro s hs
induction s, hs using MeasurableSet.induction_on_open with
| isOpen U hU => exact compl_compl U ▸ A _ hU.measurableSet.compl (h'f _ hU.isClosed_compl)
| compl s hs ihs => exact A s hs ihs
| iUnion g g_disj g_meas hg => simp [integral_iUnion g_meas g_disj hf.integrableOn, hg]
