English
If for all measurable sets s, the integral of f over s is zero, then f is zero almost everywhere with respect to μ.
Русский
Если интеграл функции f по любому измеримому множеству s равен нулю, то f = 0 a.e. по μ.
LaTeX
$$$\forall s: MeasurableSet, \int_s f \; d\mu = 0 \Rightarrow f = 0 \text{ a.e. wrt } \mu$$$
Lean4
theorem ae_eq_zero_restrict_of_forall_setIntegral_eq_zero {f : α → E}
(hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
(hf_zero : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) {t : Set α} (ht : MeasurableSet t)
(hμt : μ t ≠ ∞) : f =ᵐ[μ.restrict t] 0 :=
by
rcases (hf_int_finite t ht hμt.lt_top).aestronglyMeasurable.isSeparable_ae_range with ⟨u, u_sep, hu⟩
refine ae_eq_zero_of_forall_dual_of_isSeparable ℝ u_sep (fun c => ?_) hu
refine ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real ?_ ?_ ht hμt
· intro s hs hμs
exact ContinuousLinearMap.integrable_comp c (hf_int_finite s hs hμs)
· intro s hs hμs
rw [ContinuousLinearMap.integral_comp_comm c (hf_int_finite s hs hμs), hf_zero s hs hμs]
exact ContinuousLinearMap.map_zero _
