# 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] → ℝ`. #

source
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.

source
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.

source
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

source
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.

source
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.

source
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.

source
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.

source
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.

source
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

source
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

source
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

source
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`.

source
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`.

source
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`.

source
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`.

source
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`.

source
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`.

source
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`.

source
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`.

source
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.

source
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.

source
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`.

source
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.

source
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`.

source
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.

source
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`.

source
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.

source
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`.

source
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.

source
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`.

source
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.

source
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`.

source
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.

source
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`.

source
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 → ℝ` #

source
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.