English
If g has nonnegative right derivative on Ioo(min(a,b), max(a,b)) and the derivative is nonnegative, then g' is integrable on Ioc(a,b).
Русский
Если правая производная неотрицательна на Ioo(min(a,b), max(a,b)), то g' интегрируема на Ioc(a,b).
LaTeX
$$$\\text{IntegrableOn } g'\\ (Ioc\\ a\\ b)\\quad\\text{при } g'\\ge 0$$$
Lean4
/-- The integral of the derivative of a product of two maps.
For improper integrals, see `MeasureTheory.integral_deriv_mul_eq_sub`,
`MeasureTheory.integral_Ioi_deriv_mul_eq_sub`, and `MeasureTheory.integral_Iic_deriv_mul_eq_sub`. -/
theorem integral_deriv_mul_eq_sub_of_hasDeriv_right (hu : ContinuousOn u [[a, b]]) (hv : ContinuousOn v [[a, b]])
(huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x)
(hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x) (hu' : IntervalIntegrable u' volume a b)
(hv' : IntervalIntegrable v' volume a b) : ∫ x in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a :=
by
apply integral_eq_sub_of_hasDeriv_right (hu.mul hv) fun x hx ↦ (huu' x hx).mul (hvv' x hx)
exact (hu'.mul_continuousOn hv).add (hv'.continuousOn_mul hu)
