Documentation

Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

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.

source
theorem intervalIntegral.integral_deriv_of_contDiffOn_Icc {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (h : ContDiffOn ℝ 1 f (Set.Icc a b)) (hab : a ≤ b) :
∫ (x : ℝ) in a..b, deriv f x = f b - f a

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.

source
theorem intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (h : ContDiffOn ℝ 1 f (Set.Icc a b)) (hab : a ≤ b) :
∫ (x : ℝ) in a..b, derivWithin f (Set.Icc a b) x = f b - f a

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.

source
theorem intervalIntegral.integral_deriv_of_contDiffOn_uIcc {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (h : ContDiffOn ℝ 1 f (Set.uIcc a b)) :
∫ (x : ℝ) in a..b, deriv f x = f b - f a

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.

source
theorem intervalIntegral.integral_derivWithin_uIcc_of_contDiffOn_uIcc {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (h : ContDiffOn ℝ 1 f (Set.uIcc a b)) :
∫ (x : ℝ) in a..b, derivWithin f (Set.uIcc a b) x = f b - f a

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.

source
theorem enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (h : ContDiffOn ℝ 1 f (Set.Icc a b)) (hab : a ≤ b) :
‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Set.Icc a b, ‖deriv f x‖ₑ
source
theorem enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (h : ContDiffOn ℝ 1 f (Set.Icc a b)) (hab : a ≤ b) :
‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Set.Icc a b, ‖derivWithin f (Set.Icc a b) x‖ₑ