integral_deriv_eq_sub' — Mathlib

English

A variant of FTC on the unit interval with a prime symbol: z1 times the unit-interval integral of f'(z0 + t z1) equals f(z0+z1) − f(z0).

Русский

Вариант ФТК на единичном промежутке с производной по новой переменной: z1⋅∫_0^1 f'(z0 + t z1) dt = f(z0+z1) − f(z0).

LaTeX

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

Lean4

theorem integral_deriv_eq_sub' (f) (hderiv : deriv f = f') (hdiff : ∀ x ∈ uIcc a b, DifferentiableAt ℝ f x)
    (hcont : ContinuousOn f' (uIcc a b)) : ∫ y in a..b, f' y = f b - f a :=
  by
  rw [← hderiv, integral_deriv_eq_sub hdiff]
  rw [hderiv]
  exact hcont.intervalIntegrable

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