Documentation

Mathlib.Analysis.Calculus.LocalExtr.Rolle

Rolle's Theorem #

In this file we prove Rolle's Theorem. The theorem says that for a function f : ℝ → ℝ such that

there exists a point $c∈(a, b)$ such that $f'(c)=0$.

We prove four versions of this theorem.

References #

Tags #

local extremum, Rolle's Theorem

theorem exists_hasDerivAt_eq_zero {f : } {f' : } {a : } {b : } (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfI : f a = f b) (hff' : xSet.Ioo a b, HasDerivAt f (f' x) x) :
cSet.Ioo a b, f' c = 0

Rolle's Theorem HasDerivAt version

theorem exists_deriv_eq_zero {f : } {a : } {b : } (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfI : f a = f b) :
cSet.Ioo a b, deriv f c = 0

Rolle's Theorem deriv version

theorem exists_hasDerivAt_eq_zero' {f : } {f' : } {a : } {b : } {l : } (hab : a < b) (hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l)) (hfb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l)) (hff' : xSet.Ioo a b, HasDerivAt f (f' x) x) :
cSet.Ioo a b, f' c = 0

Rolle's Theorem, a version for a function on an open interval: if f has derivative f' on (a, b) and has the same limit l at 𝓝[>] a and 𝓝[<] b, then f' c = 0 for some c ∈ (a, b).

theorem exists_deriv_eq_zero' {f : } {a : } {b : } {l : } (hab : a < b) (hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l)) (hfb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l)) :
cSet.Ioo a b, deriv f c = 0

Rolle's Theorem, a version for a function on an open interval: if f has the same limit l at 𝓝[>] a and 𝓝[<] b, then deriv f c = 0 for some c ∈ (a, b). This version does not require differentiability of f because we define deriv f c = 0 whenever f is not differentiable at c.