integrableOn_deriv_of_nonneg — Mathlib

English

A unit-interval derivative identity holds in the 𝕜-scalar setting: with continuous-on and HasDerivAt on the unit interval, a linear combination equals the endpoints difference in a precise tensor-like form.

Русский

Тождество производной на единичном интервале сохраняется в скалярной обстановке 𝕜; линейная комбинация даёт разность концов.

LaTeX

$$$ z_1 \\int_{0}^{1} f'(z_0 + t z_1) dt = f(z_0+z_1) - f(z_0) $$$

Lean4

/-- When the derivative of a function is nonnegative, then it is automatically integrable,
Ioc version. -/
theorem integrableOn_deriv_of_nonneg (hcont : ContinuousOn g (Icc a b)) (hderiv : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x)
    (g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x) : IntegrableOn g' (Ioc a b) :=
  integrableOn_deriv_right_of_nonneg hcont (fun x hx => (hderiv x hx).hasDerivWithinAt) g'pos

Похожие утверждения