integral_eq_sub_of_hasDerivAt_of_le

English

If f extends to the boundary with limits fa, fb, under suitable differentiability and integrability, ∫ f' = fb − fa.

Русский

Если f имеет предельные значения fa и fb на границах и выполняются условия дифференцируемости и интегрируемости, то ∫ f' = fb−fa.

LaTeX

$$$\\int_{a}^{b} f'(y) dy = fb-fa \\quad\\text{where } f\\to fa \\text{ near } a^+ ,\\; f\\to fb \\text{ near } b^-.$$$

Lean4

/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is continuous on `[a, b]` (where `a ≤ b`) and
  has a derivative at `f' x` for all `x` in `(a, b)`, and `f'` is integrable on `[a, b]`, then
  `∫ y in a..b, f' y` equals `f b - f a`. -/
theorem integral_eq_sub_of_hasDerivAt_of_le (hab : a ≤ b) (hcont : ContinuousOn f (Icc a b))
    (hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' volume a b) :
    ∫ y in a..b, f' y = f b - f a :=
  integral_eq_sub_of_hasDeriv_right_of_le hab hcont (fun x hx => (hderiv x hx).hasDerivWithinAt) hint

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