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_hasDerivWithinAt_eq_of_gt_of_lt {a : ℝ} {b : ℝ} {f : ℝ → ℝ} {f' : ℝ → ℝ} (hab : a ≤ b) (hf : ∀ (x : ℝ), x ∈ Set.Icc a b → HasDerivWithinAt 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).

theorem exists_hasDerivWithinAt_eq_of_lt_of_gt {a : ℝ} {b : ℝ} {f : ℝ → ℝ} {f' : ℝ → ℝ} (hab : a ≤ b) (hf : ∀ (x : ℝ), x ∈ Set.Icc a b → HasDerivWithinAt 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).

theorem Set.OrdConnected.image_hasDerivWithinAt {f : ℝ → ℝ} {f' : ℝ → ℝ} {s : Set ℝ} (hs : Set.OrdConnected s) (hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x) : Set.OrdConnected (f' '' s)

Darboux's theorem: the image of a Set.OrdConnected set under f' is a Set.OrdConnected set, HasDerivWithinAt version.

theorem Set.OrdConnected.image_derivWithin {f : ℝ → ℝ} {s : Set ℝ} (hs : Set.OrdConnected s) (hf : DifferentiableOn ℝ f s) : Set.OrdConnected (derivWithin f s '' s)

Darboux's theorem: the image of a Set.OrdConnected set under f' is a Set.OrdConnected set, derivWithin version.

theorem Set.OrdConnected.image_deriv {f : ℝ → ℝ} {s : Set ℝ} (hs : Set.OrdConnected s) (hf : ∀ (x : ℝ), x ∈ s → DifferentiableAt ℝ f x) : Set.OrdConnected (deriv f '' s)

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

theorem Convex.image_hasDerivWithinAt {f : ℝ → ℝ} {f' : ℝ → ℝ} {s : Set ℝ} (hs : Convex ℝ s) (hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x) : Convex ℝ (f' '' s)

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

theorem Convex.image_derivWithin {f : ℝ → ℝ} {s : Set ℝ} (hs : Convex ℝ s) (hf : DifferentiableOn ℝ f s) : Convex ℝ (derivWithin f s '' s)

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

theorem Convex.image_deriv {f : ℝ → ℝ} {s : Set ℝ} (hs : Convex ℝ s) (hf : ∀ (x : ℝ), x ∈ s → DifferentiableAt ℝ f x) : Convex ℝ (deriv f '' s)

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

theorem exists_hasDerivWithinAt_eq_of_ge_of_le {a : ℝ} {b : ℝ} {f : ℝ → ℝ} {f' : ℝ → ℝ} (hab : a ≤ b) (hf : ∀ (x : ℝ), x ∈ Set.Icc a b → HasDerivWithinAt 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].

theorem exists_hasDerivWithinAt_eq_of_le_of_ge {a : ℝ} {b : ℝ} {f : ℝ → ℝ} {f' : ℝ → ℝ} (hab : a ≤ b) (hf : ∀ (x : ℝ), x ∈ Set.Icc a b → HasDerivWithinAt 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].

theorem hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne {f : ℝ → ℝ} {f' : ℝ → ℝ} {s : Set ℝ} (hs : Convex ℝ s) (hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt 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.