Theorems · Theorem · real analysis

intervalIntegral.integral_unitInterval_deriv_eq_sub

∀ {𝕜 : Type u_2} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E] [IsScalarTower ℝ 𝕜 E] {f f' : 𝕜 → E} {z₀ z₁ : 𝕜},
  ContinuousOn (fun t => f' (z₀ + t • z₁)) (Set.Icc 0 1) →
    (∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)) →
      z₁ • ∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁) = f (z₀ + z₁) - f z₀

A variant of intervalIntegral.integral_deriv_eq_sub, the Fundamental theorem of calculus, involving integrating over the unit interval.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Cited by

2 results in Mathlib

Foundations

Depth 268 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceRCLikeNormedSpaceIsScalarTower