English
If g has nonnegative right derivative on (min(a,b), max(a,b)) and is continuous on the endpoints, then the derivative is integrable on the unit-interval Ioc(a,b).
Русский
Если правая производная g по правой дуге неотрицательна на (min(a,b), max(a,b)) и непрерывна на концах, то производная интегрируема на Ioc(a,b).
LaTeX
$$$\\text{IntervalIntegrable } g'\\ (a,b)\\quad\\text{when } g'\\ge 0$$$
Lean4
/-- When the derivative of a function is nonnegative, then it is automatically integrable,
interval version. -/
theorem intervalIntegrable_deriv_of_nonneg (hcont : ContinuousOn g (uIcc a b))
(hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x) (hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x) :
IntervalIntegrable g' volume a b := by
rcases le_total a b with hab | hab
· simp only [uIcc_of_le, min_eq_left, max_eq_right, IntervalIntegrable, hab, Ioc_eq_empty_of_le, integrableOn_empty,
and_true] at hcont hderiv hpos ⊢
exact integrableOn_deriv_of_nonneg hcont hderiv hpos
· simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab, IntervalIntegrable, Ioc_eq_empty_of_le, integrableOn_empty,
true_and] at hcont hderiv hpos ⊢
exact integrableOn_deriv_of_nonneg hcont hderiv hpos
