The First- and Second-Derivative Tests

We prove the first-derivative test from calculus, in the strong form given on Wikipedia.

The test is proved over the real numbers ℝ using monotoneOn_of_deriv_nonneg from Mathlib/Analysis/Calculus/Deriv/MeanValue.lean.

We prove the second-derivative test using the first-derivative test. Source: Wikipedia.

Main results

• isLocalMax_of_deriv_Ioo: Suppose f is a real-valued function of a real variable defined on some interval containing the point a. Further suppose that f is continuous at a and differentiable on some open interval containing a, except possibly at a itself.

  If there exists a positive number r > 0 such that for every x in (a − r, a) we have f′(x) ≥ 0, and for every x in (a, a + r) we have f′(x) ≤ 0, then f has a local maximum at a.

• isLocalMin_of_deriv_Ioo: The dual of first_derivative_max, for minima.

• isLocalMax_of_deriv: 1st derivative test for maxima using filters.

• isLocalMin_of_deriv: 1st derivative test for minima using filters.

• isLocalMin_of_deriv_deriv_pos: The second-derivative test, minimum version.

Tags

derivative test, first-derivative test, second-derivative test, calculus

theorem isLocalMax_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b < c) (h : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioo b c)) (h₀ : ∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) : IsLocalMax f b

The First-Derivative Test from calculus, maxima version. Suppose a < b < c, f : ℝ → ℝ is continuous at b, the derivative f' is nonnegative on (a,b), and the derivative f' is nonpositive on (b,c). Then f has a local maximum at a.

theorem isLocalMin_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b < c) (h : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioo b c)) (h₀ : ∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) : IsLocalMin f b

The First-Derivative Test from calculus, minima version.

theorem isLocalMax_of_deriv' {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b) (hd₀ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), DifferentiableAt ℝ f x) (hd₁ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), DifferentiableAt ℝ f x) (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), 0 ≤ deriv f x) (h₁ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), deriv f x ≤ 0) : IsLocalMax f b

The First-Derivative Test from calculus, maxima version, expressed in terms of left and right filters.

theorem isLocalMin_of_deriv' {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b) (hd₀ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), DifferentiableAt ℝ f x) (hd₁ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), DifferentiableAt ℝ f x) (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), deriv f x ≤ 0) (h₁ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), deriv f x ≥ 0) : IsLocalMin f b

The First-Derivative Test from calculus, minima version, expressed in terms of left and right filters.

theorem isLocalMax_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b) (hd : ∀ᶠ (x : ℝ) in nhdsWithin b {b}ᶜ, DifferentiableAt ℝ f x) (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), 0 ≤ deriv f x) (h₁ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), deriv f x ≤ 0) : IsLocalMax f b

The First Derivative test, maximum version.

theorem isLocalMin_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b) (hd : ∀ᶠ (x : ℝ) in nhdsWithin b {b}ᶜ, DifferentiableAt ℝ f x) (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), deriv f x ≤ 0) (h₁ : ∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), 0 ≤ deriv f x) : IsLocalMin f b

The First Derivative test, minimum version.

theorem eventually_nhdsWithin_sign_eq_of_deriv_pos {f : ℝ → ℝ} {x₀ : ℝ} (hf : deriv f x₀ > 0) (hx : f x₀ = 0) : ∀ᶠ (x : ℝ) in nhds x₀, SignType.sign (f x) = SignType.sign (x - x₀)

If the derivative of f is positive at a root x₀ of f, then locally the sign of f x matches x - x₀.

theorem eventually_nhdsWithin_sign_eq_of_deriv_neg {f : ℝ → ℝ} {x₀ : ℝ} (hf : deriv f x₀ < 0) (hx : f x₀ = 0) : ∀ᶠ (x : ℝ) in nhds x₀, SignType.sign (f x) = SignType.sign (x₀ - x)

If the derivative of f is negative at a root x₀ of f, then locally the sign of f x matches x₀ - x.

theorem deriv_neg_left_of_sign_deriv {f : ℝ → ℝ} {x₀ : ℝ} (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x - x₀)) : ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Iio x₀), deriv f b < 0

theorem deriv_neg_right_of_sign_deriv {f : ℝ → ℝ} {x₀ : ℝ} (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x₀ - x)) : ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Ioi x₀), deriv f b < 0

theorem deriv_pos_right_of_sign_deriv {f : ℝ → ℝ} {x₀ : ℝ} (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x - x₀)) : ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Ioi x₀), deriv f b > 0

theorem deriv_pos_left_of_sign_deriv {f : ℝ → ℝ} {x₀ : ℝ} (h₀ : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x₀ - x)) : ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Iio x₀), deriv f b > 0

theorem isLocalMax_of_sign_deriv {f : ℝ → ℝ} {x₀ : ℝ} (h : ContinuousAt f x₀) (hf : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x₀ - x)) : IsLocalMax f x₀

The First Derivative test with a hypothesis on the sign of the derivative, maximum version.

theorem isLocalMin_of_sign_deriv {f : ℝ → ℝ} {x₀ : ℝ} (h : ContinuousAt f x₀) (hf : ∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x - x₀)) : IsLocalMin f x₀

The First Derivative test with a hypothesis on the sign of the derivative, minimum version.

theorem isLocalMin_of_deriv_deriv_pos {f : ℝ → ℝ} {x₀ : ℝ} (hf : deriv (deriv f) x₀ > 0) (hd : deriv f x₀ = 0) (hc : ContinuousAt f x₀) : IsLocalMin f x₀

The Second-Derivative Test from calculus, minimum version. Applies to functions like x^2 + 1[x ≥ 0] as well as twice differentiable functions.

theorem isLocalMax_of_deriv_deriv_neg {f : ℝ → ℝ} {x₀ : ℝ} (hf : deriv (deriv f) x₀ < 0) (hd : deriv f x₀ = 0) (hc : ContinuousAt f x₀) : IsLocalMax f x₀

The Second-Derivative Test from calculus, maximum version.