Mean value theorem

In this file we prove Cauchy's and Lagrange's mean value theorems, and deduce some corollaries.

Cauchy's mean value theorem says that for two functions f and g that are continuous on [a, b] and are differentiable on (a, b), there exists a point c ∈ (a, b) such that f' c / g' c = (f b - f a) / (g b - g a). We formulate this theorem with both sides multiplied by the denominators, see exists_ratio_hasDerivAt_eq_ratio_slope, in order to avoid auxiliary conditions like g' c ≠ 0.

Lagrange's mean value theorem, see exists_hasDerivAt_eq_slope, says that for a function f that is continuous on [a, b] and is differentiable on (a, b), there exists a point c ∈ (a, b) such that f' c = (f b - f a) / (b - a).

Lagrange's MVT implies that (f b - f a) / (b - a) > C provided that f' c > C for all c ∈ (a, b), see mul_sub_lt_image_sub_of_lt_deriv, and other theorems for > / ≥ / < / ≤.

In case C = 0, we deduce that a function with a positive derivative is strictly monotone, see strictMonoOn_of_deriv_pos and nearby theorems for other types of monotonicity.

We also prove that a real function whose derivative tends to infinity from the right at a point is not differentiable on the right at that point, and similarly differentiability on the left.

Main results

• exists_ratio_hasDerivAt_eq_ratio_slope and exists_ratio_deriv_eq_ratio_slope : Cauchy's Mean Value Theorem.

• exists_hasDerivAt_eq_slope and exists_deriv_eq_slope : Lagrange's Mean Value Theorem.

• domain_mvt : Lagrange's Mean Value Theorem, applied to a segment in a convex domain.

• Convex.image_sub_lt_mul_sub_of_deriv_lt, Convex.mul_sub_lt_image_sub_of_lt_deriv, Convex.image_sub_le_mul_sub_of_deriv_le, Convex.mul_sub_le_image_sub_of_le_deriv, if ∀ x, C (</≤/>/≥) (f' x), then C * (y - x) (</≤/>/≥) (f y - f x) whenever x < y.

• monotoneOn_of_deriv_nonneg, antitoneOn_of_deriv_nonpos, strictMono_of_deriv_pos, strictAnti_of_deriv_neg : if the derivative of a function is non-negative/non-positive/positive/negative, then the function is monotone/antitone/strictly monotone/strictly monotonically decreasing.

• convexOn_of_deriv, convexOn_of_deriv2_nonneg : if the derivative of a function is increasing or its second derivative is nonnegative, then the original function is convex.

Functions [a, b] → ℝ.

theorem exists_ratio_hasDerivAt_eq_ratio_slope (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) (g g' : ℝ → ℝ) (hgc : ContinuousOn g (Set.Icc a b)) (hgg' : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) : ∃ c ∈ Set.Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

Cauchy's Mean Value Theorem, HasDerivAt version.

theorem exists_ratio_hasDerivAt_eq_ratio_slope' (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (g g' : ℝ → ℝ) {lfa lga lfb lgb : ℝ} (hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) (hgg' : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) (hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds lfa)) (hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds lga)) (hfb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lfb)) (hgb : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds lgb)) : ∃ c ∈ Set.Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c

Cauchy's Mean Value Theorem, extended HasDerivAt version.

theorem exists_hasDerivAt_eq_slope (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) : ∃ c ∈ Set.Ioo a b, f' c = (f b - f a) / (b - a)

Lagrange's Mean Value Theorem, HasDerivAt version

theorem exists_ratio_deriv_eq_ratio_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) (g : ℝ → ℝ) (hgc : ContinuousOn g (Set.Icc a b)) (hgd : DifferentiableOn ℝ g (Set.Ioo a b)) : ∃ c ∈ Set.Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c

Cauchy's Mean Value Theorem, deriv version.

theorem exists_ratio_deriv_eq_ratio_slope' (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (g : ℝ → ℝ) {lfa lga lfb lgb : ℝ} (hdf : DifferentiableOn ℝ f (Set.Ioo a b)) (hdg : DifferentiableOn ℝ g (Set.Ioo a b)) (hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds lfa)) (hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds lga)) (hfb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lfb)) (hgb : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds lgb)) : ∃ c ∈ Set.Ioo a b, (lgb - lga) * deriv f c = (lfb - lfa) * deriv g c

Cauchy's Mean Value Theorem, extended deriv version.

theorem exists_deriv_eq_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) : ∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a)

Lagrange's Mean Value Theorem, deriv version.

theorem exists_deriv_eq_slope' (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) : ∃ c ∈ Set.Ioo a b, deriv f c = slope f a b

Lagrange's Mean Value Theorem, deriv version.

theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi (f : ℝ → ℝ) {a : ℝ} (hf : Filter.Tendsto (deriv f) (nhdsWithin a (Set.Ioi a)) Filter.atTop) : ¬DifferentiableWithinAt ℝ f (Set.Ioi a) a

A real function whose derivative tends to infinity from the right at a point is not differentiable on the right at that point.

theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi (f : ℝ → ℝ) {a : ℝ} (hf : Filter.Tendsto (deriv f) (nhdsWithin a (Set.Ioi a)) Filter.atBot) : ¬DifferentiableWithinAt ℝ f (Set.Ioi a) a

A real function whose derivative tends to minus infinity from the right at a point is not differentiable on the right at that point

theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio (f : ℝ → ℝ) {a : ℝ} (hf : Filter.Tendsto (deriv f) (nhdsWithin a (Set.Iio a)) Filter.atBot) : ¬DifferentiableWithinAt ℝ f (Set.Iio a) a

A real function whose derivative tends to minus infinity from the left at a point is not differentiable on the left at that point

theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio (f : ℝ → ℝ) {a : ℝ} (hf : Filter.Tendsto (deriv f) (nhdsWithin a (Set.Iio a)) Filter.atTop) : ¬DifferentiableWithinAt ℝ f (Set.Iio a) a

A real function whose derivative tends to infinity from the left at a point is not differentiable on the left at that point

theorem Convex.mul_sub_lt_image_sub_of_lt_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C : ℝ} (hf'_gt : ∀ x ∈ interior D, C < deriv f x) (x : ℝ) : x ∈ D → ∀ y ∈ D, x < y → C * (y - x) < f y - f x

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and C < f', then f grows faster than C * x on D, i.e., C * (y - x) < f y - f x whenever x, y ∈ D, x < y.

theorem mul_sub_lt_image_sub_of_lt_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C : ℝ} (hf'_gt : ∀ (x : ℝ), C < deriv f x) ⦃x y : ℝ⦄ (hxy : x < y) : C * (y - x) < f y - f x

Let f : ℝ → ℝ be a differentiable function. If C < f', then f grows faster than C * x, i.e., C * (y - x) < f y - f x whenever x < y.

theorem Convex.mul_sub_le_image_sub_of_le_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C : ℝ} (hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x) (x : ℝ) : x ∈ D → ∀ y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and C ≤ f', then f grows at least as fast as C * x on D, i.e., C * (y - x) ≤ f y - f x whenever x, y ∈ D, x ≤ y.

theorem mul_sub_le_image_sub_of_le_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C : ℝ} (hf'_ge : ∀ (x : ℝ), C ≤ deriv f x) ⦃x y : ℝ⦄ (hxy : x ≤ y) : C * (y - x) ≤ f y - f x

Let f : ℝ → ℝ be a differentiable function. If C ≤ f', then f grows at least as fast as C * x, i.e., C * (y - x) ≤ f y - f x whenever x ≤ y.

theorem Convex.image_sub_lt_mul_sub_of_deriv_lt {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C : ℝ} (lt_hf' : ∀ x ∈ interior D, deriv f x < C) (x : ℝ) (hx : x ∈ D) (y : ℝ) (hy : y ∈ D) (hxy : x < y) : f y - f x < C * (y - x)

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' < C, then f grows slower than C * x on D, i.e., f y - f x < C * (y - x) whenever x, y ∈ D, x < y.

theorem image_sub_lt_mul_sub_of_deriv_lt {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C : ℝ} (lt_hf' : ∀ (x : ℝ), deriv f x < C) ⦃x y : ℝ⦄ (hxy : x < y) : f y - f x < C * (y - x)

Let f : ℝ → ℝ be a differentiable function. If f' < C, then f grows slower than C * x on D, i.e., f y - f x < C * (y - x) whenever x < y.

theorem Convex.image_sub_le_mul_sub_of_deriv_le {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C : ℝ} (le_hf' : ∀ x ∈ interior D, deriv f x ≤ C) (x : ℝ) (hx : x ∈ D) (y : ℝ) (hy : y ∈ D) (hxy : x ≤ y) : f y - f x ≤ C * (y - x)

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' ≤ C, then f grows at most as fast as C * x on D, i.e., f y - f x ≤ C * (y - x) whenever x, y ∈ D, x ≤ y.

theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C : ℝ} (le_hf' : ∀ (x : ℝ), deriv f x ≤ C) ⦃x y : ℝ⦄ (hxy : x ≤ y) : f y - f x ≤ C * (y - x)

Let f : ℝ → ℝ be a differentiable function. If f' ≤ C, then f grows at most as fast as C * x, i.e., f y - f x ≤ C * (y - x) whenever x ≤ y.

theorem strictMonoOn_of_deriv_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, 0 < deriv f x) : StrictMonoOn f D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is positive, then f is a strictly monotone function on D. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly positive.

theorem strictMono_of_deriv_pos {f : ℝ → ℝ} (hf' : ∀ (x : ℝ), 0 < deriv f x) : StrictMono f

Let f : ℝ → ℝ be a differentiable function. If f' is positive, then f is a strictly monotone function. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly positive.

theorem strictMonoOn_of_hasDerivWithinAt_pos {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : ∀ x ∈ interior D, 0 < f' x) : StrictMonoOn f D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is strictly positive, then f is a strictly monotone function on D.

theorem strictMono_of_hasDerivAt_pos {f f' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), 0 < f' x) : StrictMono f

Let f : ℝ → ℝ be a differentiable function. If f' is strictly positive, then f is a strictly monotone function.

theorem monotoneOn_of_deriv_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x) : MonotoneOn f D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is nonnegative, then f is a monotone function on D.

theorem monotone_of_deriv_nonneg {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf' : ∀ (x : ℝ), 0 ≤ deriv f x) : Monotone f

Let f : ℝ → ℝ be a differentiable function. If f' is nonnegative, then f is a monotone function.

theorem monotoneOn_of_hasDerivWithinAt_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x) : MonotoneOn f D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is nonnegative, then f is a monotone function on D.

theorem monotone_of_hasDerivAt_nonneg {f f' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : 0 ≤ f') : Monotone f

Let f : ℝ → ℝ be a differentiable function. If f' is nonnegative, then f is a monotone function.

theorem strictAntiOn_of_deriv_neg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, deriv f x < 0) : StrictAntiOn f D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is negative, then f is a strictly antitone function on D.

theorem strictAnti_of_deriv_neg {f : ℝ → ℝ} (hf' : ∀ (x : ℝ), deriv f x < 0) : StrictAnti f

Let f : ℝ → ℝ be a differentiable function. If f' is negative, then f is a strictly antitone function. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly negative.

theorem strictAntiOn_of_hasDerivWithinAt_neg {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : ∀ x ∈ interior D, f' x < 0) : StrictAntiOn f D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is strictly positive, then f is a strictly monotone function on D.

theorem strictAnti_of_hasDerivAt_neg {f f' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), f' x < 0) : StrictAnti f

Let f : ℝ → ℝ be a differentiable function. If f' is strictly positive, then f is a strictly monotone function.

theorem antitoneOn_of_deriv_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) : AntitoneOn f D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is nonpositive, then f is an antitone function on D.

theorem antitone_of_deriv_nonpos {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf' : ∀ (x : ℝ), deriv f x ≤ 0) : Antitone f

Let f : ℝ → ℝ be a differentiable function. If f' is nonpositive, then f is an antitone function.

theorem antitoneOn_of_hasDerivWithinAt_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : ∀ x ∈ interior D, f' x ≤ 0) : AntitoneOn f D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is nonpositive, then f is an antitone function on D.

theorem antitone_of_hasDerivAt_nonpos {f f' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : f' ≤ 0) : Antitone f

Let f : ℝ → ℝ be a differentiable function. If f' is nonpositive, then f is an antitone function.

Functions f : E → ℝ

theorem domain_mvt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x y : E} {f' : E → StrongDual ℝ E} (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) : ∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)

Lagrange's Mean Value Theorem, applied to convex domains.