Rolle's Theorem

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

• $f$ is differentiable on an open interval $(a, b)$, $a < b$;
• $f$ is continuous on the corresponding closed interval $[a, b]$;
• $f(a) = f(b)$,

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

We prove four versions of this theorem.

• exists_hasDerivAt_eq_zero is closest to the statement given above. It assumes that at every point $x ∈ (a, b)$ function $f$ has derivative $f'(x)$, then concludes that $f'(c)=0$ for some $c∈(a, b)$.
• exists_deriv_eq_zero deals with deriv f instead of an arbitrary function f' and a predicate has_deriv_at; since we use zero as the "junk" value for deriv f c, this version does not assume that f is differentiable on the open interval.
• exists_hasDerivAt_eq_zero' is similar to exists_hasDerivAt_eq_zero but instead of assuming continuity on the closed interval $[a, b]$ it assumes that $f$ tends to the same limit as $x$ tends to $a$ from the right and as $x$ tends to $b$ from the left.
• exists_deriv_eq_zero' relates to exists_deriv_eq_zero as exists_hasDerivAt_eq_zero' relates to ``exists_hasDerivAt_eq_zero`.

References

• Rolle's Theorem;

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' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) : ∃ c ∈ Set.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) : ∃ c ∈ Set.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' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) : ∃ c ∈ Set.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)) : ∃ c ∈ Set.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.