theorem relative_extremum_def (f : ℝ → ℝ) (S : Set ℝ) (c : ℝ) (_hc : c ∈ S) : (IsLocalMaxOn f S c ↔ ∃ δ > 0, ∀ x ∈ S, |x - c| < δ → f x ≤ f c) ∧ (IsLocalMinOn f S c ↔ ∃ δ > 0, ∀ x ∈ S, |x - c| < δ → f c ≤ f x)

Characterization of relative extrema in terms of an explicit δ-neighborhood. For f : ℝ → ℝ, S ⊆ ℝ, and c ∈ S: f has a relative maximum at c on S (IsLocalMaxOn f S c) iff there exists δ > 0 such that for all x ∈ S with |x - c| < δ, f x ≤ f c; and analogously, f has a relative minimum at c on S iff there exists δ > 0 such that for all x ∈ S with |x - c| < δ, f c ≤ f x.

theorem fermats_theorem (f : ℝ → ℝ) (c : ℝ) (hext : IsLocalMax f c ∨ IsLocalMin f c) (_hd : DifferentiableAt ℝ f c) : deriv f c = 0

Fermat's interior extremum theorem: if f : ℝ → ℝ attains a (global) local maximum or local minimum at an interior point c, and f is differentiable at c, then the derivative of f at c vanishes, i.e. deriv f c = 0.

theorem rolle (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (_hfd : ∀ x ∈ Set.Ioo a b, DifferentiableAt ℝ f x) (heq : f a = f b) : ∃ c ∈ Set.Ioo a b, deriv f c = 0

Rolle's theorem: if f : ℝ → ℝ is continuous on the closed interval [a, b], differentiable at every point of the open interval (a, b), and satisfies f a = f b, then there exists some c ∈ (a, b) at which the derivative vanishes, i.e. deriv f c = 0.

theorem mean_value_theorem (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : ∀ x ∈ Set.Ioo a b, DifferentiableAt ℝ f x) : ∃ c ∈ Set.Ioo a b, f b - f a = deriv f c * (b - a)

The Mean Value Theorem: if f : ℝ → ℝ is continuous on [a, b] and differentiable at every point of (a, b), then there exists some c ∈ (a, b) such that f b - f a = deriv f c * (b - a).

theorem zero_deriv_imp_constant (f : ℝ → ℝ) (I : Set ℝ) (hI : Convex ℝ I) (hfd : DifferentiableOn ℝ f I) (hf' : ∀ x ∈ I, deriv f x = 0) (x : ℝ) : x ∈ I → ∀ y ∈ I, f x = f y

Zero derivative implies constant: if f : ℝ → ℝ is differentiable on a convex set I ⊆ ℝ (i.e. an interval) and deriv f x = 0 for every x ∈ I, then f is constant on I, i.e. f x = f y for all x, y ∈ I.

theorem monotonicity_and_derivatives (f : ℝ → ℝ) (a b : ℝ) (_hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : ∀ x ∈ Set.Ioo a b, DifferentiableAt ℝ f x) : (MonotoneOn f (Set.Icc a b) ↔ ∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) ∧ (AntitoneOn f (Set.Icc a b) ↔ ∀ x ∈ Set.Ioo a b, deriv f x ≤ 0)

Monotonicity characterized by the sign of the derivative on an interval. If f : ℝ → ℝ is continuous on [a, b] and differentiable at every point of (a, b), then: (1) f is monotonically increasing on [a, b] iff 0 ≤ deriv f x for all x ∈ (a, b); (2) f is monotonically decreasing on [a, b] iff deriv f x ≤ 0 for all x ∈ (a, b).