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 Ioo (a − r) a we have f′(x) ≥ 0, and for every x in Ioo 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 isMaxOn_Ioo_of_deriv {f : ℝ → ℝ} {a 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) : IsMaxOn f (Set.Ioo a c) b

Suppose f : ℝ → ℝ is continuous at b, the derivative f' is nonnegative on Ioo a b and nonpositive on Ioo b c. Then f attains its maximum on Ioo a c at b.

theorem isMaxOn_Ioc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c) (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) : IsMaxOn f (Set.Ioc a c) b

Suppose f : ℝ → ℝ is continuous at b and c, the derivative f' is nonnegative on Ioo a b and nonpositive on Ioo b c. Then f attains its maximum on Ioc a c at b.

theorem isMaxOn_Ico_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : 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) : IsMaxOn f (Set.Ico a c) b

Suppose f : ℝ → ℝ is continuous at a and b, the derivative f' is nonnegative on Ioo a b and nonpositive on Ioo b c. Then f attains its maximum on Ico a c at b.

theorem isMaxOn_Icc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b) (hc : ContinuousAt f c) (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) : IsMaxOn f (Set.Icc a c) b

Suppose f : ℝ → ℝ is continuous at a, b, and c, the derivative f' is nonnegative on Ioo a b and nonpositive on Ioo b c. Then f attains its maximum on Icc a c at b.

theorem isMaxOn_Ioi_of_deriv {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioi b)) (h₀ : ∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Set.Ioi b, deriv f x ≤ 0) : IsMaxOn f (Set.Ioi a) b

Suppose f : ℝ → ℝ is continuous at b, the derivative f' is nonnegative on Ioo a b and nonpositive on Ioi b. Then f attains its maximum on Ioi a at b.

theorem isMaxOn_Ici_of_deriv {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioi b)) (h₀ : ∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Set.Ioi b, deriv f x ≤ 0) : IsMaxOn f (Set.Ici a) b

Suppose f : ℝ → ℝ is continuous at a and b, the derivative f' is nonnegative on Ioo a b and nonpositive on Ioi b. Then f attains its maximum on Ici a at b.

theorem isMaxOn_Iio_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Iio b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioo b c)) (h₀ : ∀ x ∈ Set.Iio b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) : IsMaxOn f (Set.Iio c) b

Suppose f : ℝ → ℝ is continuous at b, the derivative f' is nonnegative on Iio b and nonpositive on Ioo b c. Then f attains its maximum on Iio c at b.

theorem isMaxOn_Iic_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c) (hd₀ : DifferentiableOn ℝ f (Set.Iio b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioo b c)) (h₀ : ∀ x ∈ Set.Iio b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) : IsMaxOn f (Set.Iic c) b

Suppose f : ℝ → ℝ is continuous at b and c, the derivative f' is nonnegative on Iio b and nonpositive on Ioo b c. Then f attains its maximum on Iic c at b.

theorem isMaxOn_univ_of_deriv {f : ℝ → ℝ} {b : ℝ} (hb : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Iio b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioi b)) (h₀ : ∀ x ∈ Set.Iio b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Set.Ioi b, deriv f x ≤ 0) : IsMaxOn f Set.univ b

Suppose f : ℝ → ℝ is continuous at b, the derivative f' is nonnegative on Iio b and nonpositive on Ioi b. Then f attains its maximum on ℝ at b.

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 Ioo a b and nonpositive on Ioo b c. Then f has a local maximum at b.

theorem isMinOn_Ioo_of_deriv {f : ℝ → ℝ} {a 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) : IsMinOn f (Set.Ioo a c) b

Suppose f : ℝ → ℝ is continuous at b, the derivative f' is nonpositive on Ioo a b and nonnegative on Ioo b c. Then f attains its minimum on Ioo a c at b.

theorem isMinOn_Ioc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c) (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) : IsMinOn f (Set.Ioc a c) b

Suppose f : ℝ → ℝ is continuous at b and c, the derivative f' is nonpositive on Ioo a b and nonnegative on Ioo b c. Then f attains its minimum on Ioc a c at b.

theorem isMinOn_Ico_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : 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) : IsMinOn f (Set.Ico a c) b

Suppose f : ℝ → ℝ is continuous at a and b, the derivative f' is nonpositive on Ioo a b and nonnegative on Ioo b c. Then f attains its minimum on Ico a c at b.

theorem isMinOn_Icc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b) (hc : ContinuousAt f c) (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) : IsMinOn f (Set.Icc a c) b

Suppose f : ℝ → ℝ is continuous at a, b, and c, the derivative f' is nonpositive on Ioo a b and nonnegative on Ioo b c. Then f attains its minimum on Icc a c at b.

theorem isMinOn_Ioi_of_deriv {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioi b)) (h₀ : ∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Set.Ioi b, 0 ≤ deriv f x) : IsMinOn f (Set.Ioi a) b

Suppose f : ℝ → ℝ is continuous at b, the derivative f' is nonpositive on Ioo a b and nonnegative on Ioi b. Then f attains its minimum on Ioi a at b.

theorem isMinOn_Ici_of_deriv {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioi b)) (h₀ : ∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Set.Ioi b, 0 ≤ deriv f x) : IsMinOn f (Set.Ici a) b

Suppose f : ℝ → ℝ is continuous at a and b, the derivative f' is nonpositive on Ioo a b and nonnegative on Ioi b. Then f attains its minimum on Ici a at b.

theorem isMinOn_Iio_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Iio b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioo b c)) (h₀ : ∀ x ∈ Set.Iio b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) : IsMinOn f (Set.Iio c) b

Suppose f : ℝ → ℝ is continuous at b, the derivative f' is nonpositive on Iio b and nonnegative on Ioo b c. Then f attains its minimum on Iio c at b.

theorem isMinOn_Iic_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c) (hd₀ : DifferentiableOn ℝ f (Set.Iio b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioo b c)) (h₀ : ∀ x ∈ Set.Iio b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) : IsMinOn f (Set.Iic c) b

Suppose f : ℝ → ℝ is continuous at b and c, the derivative f' is nonpositive on Iio b and nonnegative on Ioo b c. Then f attains its minimum on Iic c at b.

theorem isMinOn_univ_of_deriv {f : ℝ → ℝ} {b : ℝ} (hb : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Set.Iio b)) (hd₁ : DifferentiableOn ℝ f (Set.Ioi b)) (h₀ : ∀ x ∈ Set.Iio b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Set.Ioi b, 0 ≤ deriv f x) : IsMinOn f Set.univ b

Suppose f : ℝ → ℝ is continuous at b, the derivative f' is nonpositive on Iio b and nonnegative on Ioi b. Then f attains its minimum on ℝ at b.

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.