The First-Derivative Test

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

The test is proved over the real numbers ℝ using monotoneOn_of_deriv_nonneg from [Mathlib.Analysis.Calculus.MeanValue].

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.

Tags

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.