English
Let f be nonnegative almost everywhere on the unordered interval between a and b and assume f is integrable on [a,b]. Then the integral ∫_a^b f is zero if and only if f is equal to 0 almost everywhere on the union of the two half-intervals Ioc(a,b) ∪ Ioc(b,a).
Русский
Пусть f неотрицательно почти всюду на неупорядоченном интервалe между a и b и допускается интегрируемость f на [a,b]. Тогда интеграл ∫_a^b f равен нулю тогда и только тогда, когда f равно нулю почти всюду на объединении неполузакрытых интервалов Ioc(a,b) ∪ Ioc(b,a).
LaTeX
$$$0 \\le\\!^\\ast_{\\mu \\restriction (Ioc(a,b) \\cup Ioc(b,a))} f \\;\\wedge\\; \\text{IntervalIntegrable } f \\; \\mu\\; a,b\\quad\\Longrightarrow\\quad (\\int_a^b f\\,d\\mu = 0) \\iff (f =\\!^\\ast_{\\mu \\restriction (Ioc(a,b) \\cup Ioc(b,a))} 0)$.$$
Lean4
theorem integral_eq_zero_iff_of_nonneg_ae (hf : 0 ≤ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] f)
(hfi : IntervalIntegrable f μ a b) : ∫ x in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] 0 :=
by
rcases le_total a b with hab | hab <;> simp only [Ioc_eq_empty hab.not_gt, empty_union, union_empty] at hf ⊢
· exact integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi
· rw [integral_symm, neg_eq_zero, integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm]
