English
Let f be nonnegative almost everywhere and interval-integrable on a..b. Then the integral ∫_a^b f is positive if and only if a < b and the measure of the set {x ∈ Ioc a b | f(x) > 0} is positive.
Русский
Пусть f неотрицательно почти всюду и интегрируема на отрезке a..b. Тогда интеграл ∫_a^b f положителен тогда и только тогда, когда a < b и мера множества {x ∈ Ioc a b | f(x) > 0} положительна.
LaTeX
$$$0 < \\int_{a}^{b} f \\; d\\mu \\quad\\Longleftrightarrow\\quad a < b \\;\\wedge\\; 0 < \\mu(\\mathrm{supp}(f) \\cap Ioc(a,b)).$$$
Lean4
/-- If `f` is nonnegative and integrable on the unordered interval `Set.uIoc a b`, then its
integral over `a..b` is positive if and only if `a < b` and the measure of
`Function.support f ∩ Set.Ioc a b` is positive. -/
theorem integral_pos_iff_support_of_nonneg_ae' (hf : 0 ≤ᵐ[μ.restrict (Ι a b)] f) (hfi : IntervalIntegrable f μ a b) :
(0 < ∫ x in a..b, f x ∂μ) ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b) :=
by
rcases lt_or_ge a b with hab | hba
· rw [uIoc_of_le hab.le] at hf
simp only [hab, true_and, integral_of_le hab.le, setIntegral_pos_iff_support_of_nonneg_ae hf hfi.1]
· suffices (∫ x in a..b, f x ∂μ) ≤ 0 by simp only [this.not_gt, hba.not_gt, false_and]
rw [integral_of_ge hba, neg_nonpos]
rw [uIoc_comm, uIoc_of_le hba] at hf
exact integral_nonneg_of_ae hf
