mathlib documentation

analysis.calculus.darboux

Darboux's theorem

In this file we prove that the derivative of a differentiable function on an interval takes all intermediate values. The proof is based on the Wikipedia page about this theorem.

theorem exists_has_deriv_within_at_eq_of_gt_of_lt {a b : } {f f' : } (hab : a b) (hf : ∀ (x : ), x set.Icc a bhas_deriv_within_at f (f' x) (set.Icc a b) x) {m : } :
f' a < mm < f' bm f' '' set.Icc a b

Darboux's theorem: if a ≤ b and f' a < m < f' b, then f' c = m for some c ∈ [a, b].

theorem exists_has_deriv_within_at_eq_of_lt_of_gt {a b : } {f f' : } (hab : a b) (hf : ∀ (x : ), x set.Icc a bhas_deriv_within_at f (f' x) (set.Icc a b) x) {m : } :
m < f' af' b < mm f' '' set.Icc a b

Darboux's theorem: if a ≤ b and f' a > m > f' b, then f' c = m for some c ∈ [a, b].

theorem convex_image_has_deriv_at {f f' : } {s : set } :
convex s(∀ (x : ), x shas_deriv_at f (f' x) x)convex (f' '' s)

Darboux's theorem: the image of a convex set under f' is a convex set.

theorem deriv_forall_lt_or_forall_gt_of_forall_ne {f f' : } {s : set } (hs : convex s) (hf : ∀ (x : ), x shas_deriv_at f (f' x) x) {m : } :
(∀ (x : ), x sf' x m)((∀ (x : ), x sf' x < m) ∀ (x : ), x sm < f' x)

If the derivative of a function is never equal to m, then either it is always greater than m, or it is always less than m.