English
If f is interval-integrable on [a,b] and nonnegative almost everywhere on Ioc(a,b), then the integral ∫_a^b f ≥ 0.
Русский
Если f интегрируема на [a,b] и неотрицательна почти всюду на Ioc(a,b), то интеграл неотрицателен.
LaTeX
$$$hab: a \\le b,\\ hf: 0 \\le^*_{\\mu.restrict(Ioc(a,b))} f\\;⇒\\; 0 ≤ ∫_a^b f \\; d\\mu$$$
Lean4
/-- If `f` and `g` are two functions that are interval integrable on `a..b`, `a ≤ b`,
`f x ≤ g x` for a.e. `x ∈ Set.Ioc a b`, and `f x < g x` on a subset of `Set.Ioc a b`
of nonzero measure, then `∫ x in a..b, f x ∂μ < ∫ x in a..b, g x ∂μ`. -/
theorem integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero (hab : a ≤ b) (hfi : IntervalIntegrable f μ a b)
(hgi : IntervalIntegrable g μ a b) (hle : f ≤ᵐ[μ.restrict (Ioc a b)] g)
(hlt : μ.restrict (Ioc a b) {x | f x < g x} ≠ 0) : (∫ x in a..b, f x ∂μ) < ∫ x in a..b, g x ∂μ :=
by
rw [← sub_pos, ← integral_sub hgi hfi, integral_of_le hab, MeasureTheory.integral_pos_iff_support_of_nonneg_ae]
· refine pos_iff_ne_zero.2 (mt (measure_mono_null ?_) hlt)
exact fun x hx => (sub_pos.2 hx.out).ne'
exacts [hle.mono fun x => sub_nonneg.2, hgi.1.sub hfi.1]
