Darboux's theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem exists_has_deriv_within_at_eq_of_gt_of_lt {a b : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b) (hf : ∀ (x : ℝ), x ∈ set.Icc a b → has_deriv_within_at f (f' x) (set.Icc a b) x) {m : ℝ} (hma : f' a < m) (hmb : m < f' b) :

m ∈ f' '' set.Ioo a b

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

source

theorem exists_has_deriv_within_at_eq_of_lt_of_gt {a b : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b) (hf : ∀ (x : ℝ), x ∈ set.Icc a b → has_deriv_within_at f (f' x) (set.Icc a b) x) {m : ℝ} (hma : m < f' a) (hmb : f' b < m) :

m ∈ f' '' set.Ioo a b

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

source

theorem set.ord_connected.image_has_deriv_within_at {f f' : ℝ → ℝ} {s : set ℝ} (hs : s.ord_connected) (hf : ∀ (x : ℝ), x ∈ s → has_deriv_within_at f (f' x) s x) :

(f' '' s).ord_connected

Darboux's theorem: the image of an ord_connected set under f' is an ord_connected set, has_deriv_within_at version.

source

theorem set.ord_connected.image_deriv_within {f : ℝ → ℝ} {s : set ℝ} (hs : s.ord_connected) (hf : differentiable_on ℝ f s) :

(deriv_within f s '' s).ord_connected

Darboux's theorem: the image of an ord_connected set under f' is an ord_connected set, deriv_within version.

source

theorem set.ord_connected.image_deriv {f : ℝ → ℝ} {s : set ℝ} (hs : s.ord_connected) (hf : ∀ (x : ℝ), x ∈ s → differentiable_at ℝ f x) :

(deriv f '' s).ord_connected

Darboux's theorem: the image of an ord_connected set under f' is an ord_connected set, deriv version.

source

theorem convex.image_has_deriv_within_at {f f' : ℝ → ℝ} {s : set ℝ} (hs : convex ℝ s) (hf : ∀ (x : ℝ), x ∈ s → has_deriv_within_at f (f' x) s x) :

convex ℝ (f' '' s)

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

source

theorem convex.image_deriv_within {f : ℝ → ℝ} {s : set ℝ} (hs : convex ℝ s) (hf : differentiable_on ℝ f s) :

convex ℝ (deriv_within f s '' s)

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

source

theorem convex.image_deriv {f : ℝ → ℝ} {s : set ℝ} (hs : convex ℝ s) (hf : ∀ (x : ℝ), x ∈ s → differentiable_at ℝ f x) :

convex ℝ (deriv f '' s)

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

source

theorem exists_has_deriv_within_at_eq_of_ge_of_le {a b : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b) (hf : ∀ (x : ℝ), x ∈ set.Icc a b → has_deriv_within_at f (f' x) (set.Icc a b) x) {m : ℝ} (hma : f' a ≤ m) (hmb : m ≤ f' b) :

m ∈ 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].

source

theorem exists_has_deriv_within_at_eq_of_le_of_ge {a b : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b) (hf : ∀ (x : ℝ), x ∈ set.Icc a b → has_deriv_within_at f (f' x) (set.Icc a b) x) {m : ℝ} (hma : f' a ≤ m) (hmb : m ≤ f' b) :

m ∈ f' '' set.Icc a b

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

source

theorem has_deriv_within_at_forall_lt_or_forall_gt_of_forall_ne {f f' : ℝ → ℝ} {s : set ℝ} (hs : convex ℝ s) (hf : ∀ (x : ℝ), x ∈ s → has_deriv_within_at f (f' x) s x) {m : ℝ} (hf' : ∀ (x : ℝ), x ∈ s → f' x ≠ m) :

(∀ (x : ℝ), x ∈ s → f' x < m) ∨ ∀ (x : ℝ), x ∈ s → m < 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.