Fundamental theorem of calculus for C^1 functions #
We give versions of the second fundamental theorem of calculus under the strong assumption
that the function is C^1 on the interval. This is restrictive, but satisfied in many situations.
theorem
intervalIntegral.integral_deriv_of_contDiffOn_Icc
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{a b : ℝ}
[CompleteSpace E]
(h : ContDiffOn ℝ 1 f (Set.Icc a b))
(hab : a ≤ b)
:
Fundamental theorem of calculus-2: If f : ℝ → E is C^1 on [a, b],
then ∫ y in a..b, deriv f y equals f b - f a.
theorem
intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{a b : ℝ}
[CompleteSpace E]
(h : ContDiffOn ℝ 1 f (Set.Icc a b))
(hab : a ≤ b)
:
Fundamental theorem of calculus-2: If f : ℝ → E is C^1 on [a, b],
then ∫ y in a..b, derivWithin f (Icc a b) y equals f b - f a.
theorem
intervalIntegral.integral_deriv_of_contDiffOn_uIcc
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{a b : ℝ}
[CompleteSpace E]
(h : ContDiffOn ℝ 1 f (Set.uIcc a b))
:
Fundamental theorem of calculus-2: If f : ℝ → E is C^1 on [a, b],
then ∫ y in a..b, deriv f y equals f b - f a.
theorem
intervalIntegral.integral_derivWithin_uIcc_of_contDiffOn_uIcc
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{a b : ℝ}
[CompleteSpace E]
(h : ContDiffOn ℝ 1 f (Set.uIcc a b))
:
Fundamental theorem of calculus-2: If f : ℝ → E is C^1 on [a, b],
then ∫ y in a..b, derivWithin f (uIcc a b) y equals f b - f a.
theorem
enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{a b : ℝ}
(h : ContDiffOn ℝ 1 f (Set.Icc a b))
(hab : a ≤ b)
: