Local extrema and the second-derivative test

DefinitionStrict local minimum#✓fully proved

Let \(f \colon X \to Y\) be a function from a topological space \(X\) to a set \(Y\) equipped with a relation \(<\). Then \(f\) has a strict local minimum at a point \(a \in X\) if \(f(a) < f(x)\) for all \(x \ne a\) in some neighborhood of \(a\).

This strengthens the usual (non-strict) notion of local minimum: the inequality is strict and the point \(a\) itself is excluded.

def IsStrictLocalMin {α : Type*} {β : Type*} [TopologicalSpace α] [LT β]
    (f : α → β) (a : α) : Prop :=
  ∀ᶠ x in 𝓝[≠] a, f a < f x

Used by 4

Used byA strict local minimum is a local minimum · Strict second-derivative test, minimum version · Negation turns a strict local minimum into a strict local maximum · Negation turns a strict local maximum into a strict local minimum

DefinitionStrict local maximum#✓fully proved

Let \(f \colon X \to Y\) be a function from a topological space \(X\) to a set \(Y\) equipped with a relation \(<\). Then \(f\) has a strict local maximum at a point \(a \in X\) if \(f(x) < f(a)\) for all \(x \ne a\) in some neighborhood of \(a\).

def IsStrictLocalMax {α : Type*} {β : Type*} [TopologicalSpace α] [LT β]
    (f : α → β) (a : α) : Prop :=
  ∀ᶠ x in 𝓝[≠] a, f x < f a

Used by 4

Used byA strict local maximum is a local maximum · Strict second-derivative test, maximum version · Negation turns a strict local minimum into a strict local maximum · Negation turns a strict local maximum into a strict local minimum

TheoremA strict local minimum is a local minimum#✓fully proved

Let \(f \colon X \to Y\) be a function from a topological space \(X\) to a preordered set \(Y\). If \(f\) has a strict local minimum at \(a \in X\), then \(f\) has a local minimum at \(a\), that is, \(f(a) \le f(x)\) for all \(x\) in some neighborhood of \(a\).

theorem IsStrictLocalMin.isLocalMin {α : Type*} {β : Type*}
    [TopologicalSpace α] [Preorder β] {f : α → β} {a : α}
    (h : IsStrictLocalMin f a) : IsLocalMin f a

Uses 1

Statement usesStrict local minimum

TheoremA strict local maximum is a local maximum#✓fully proved

Let \(f \colon X \to Y\) be a function from a topological space \(X\) to a preordered set \(Y\). If \(f\) has a strict local maximum at \(a \in X\), then \(f\) has a local maximum at \(a\), that is, \(f(x) \le f(a)\) for all \(x\) in some neighborhood of \(a\).

theorem IsStrictLocalMax.isLocalMax {α : Type*} {β : Type*}
    [TopologicalSpace α] [Preorder β] {f : α → β} {a : α}
    (h : IsStrictLocalMax f a) : IsLocalMax f a

Uses 1

Statement usesStrict local maximum

TheoremNegation turns a strict local minimum into a strict local maximum#✓fully proved

Let \(X\) be a topological space and let \(Y\) be an additive group with a relation \(<\) such that addition on the left and addition on the right are strictly monotone. If \(f \colon X \to Y\) has a strict local minimum at \(a \in X\), then \(x \mapsto -f(x)\) has a strict local maximum at \(a\).

theorem IsStrictLocalMin.neg {α : Type*} {β : Type*} [TopologicalSpace α]
    [AddGroup β] [LT β] [AddLeftStrictMono β] [AddRightStrictMono β]
    {f : α → β} {a : α} (h : IsStrictLocalMin f a) :
    IsStrictLocalMax (fun x => -f x) a

Uses 2 · Used by 1

Statement usesStrict local maximum · Strict local minimum

Used byStrict second-derivative test, maximum version

TheoremNegation turns a strict local maximum into a strict local minimum#✓fully proved

Let \(X\) be a topological space and let \(Y\) be an additive group with a relation \(<\) such that addition on the left and addition on the right are strictly monotone. If \(f \colon X \to Y\) has a strict local maximum at \(a \in X\), then \(x \mapsto -f(x)\) has a strict local minimum at \(a\).

theorem IsStrictLocalMax.neg {α : Type*} {β : Type*} [TopologicalSpace α]
    [AddGroup β] [LT β] [AddLeftStrictMono β] [AddRightStrictMono β]
    {f : α → β} {a : α} (h : IsStrictLocalMax f a) :
    IsStrictLocalMin (fun x => -f x) a

Uses 2

Statement usesStrict local maximum · Strict local minimum

TheoremStrict second-derivative test, minimum version#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) and \(x_0 \in \mathbb{R}\). If \(f''(x_0) > 0\), \(f'(x_0) = 0\), and \(f\) is continuous at \(x_0\), then \(f\) has a strict local minimum at \(x_0\).

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

Uses 1 · Used by 1

Statement usesStrict local minimum

Used byStrict second-derivative test, maximum version

TheoremStrict second-derivative test, maximum version#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) and \(x_0 \in \mathbb{R}\). If \(f''(x_0) < 0\), \(f'(x_0) = 0\), and \(f\) is continuous at \(x_0\), then \(f\) has a strict local maximum at \(x_0\).

This is the minimum version applied to \(-f\).

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

Uses 3

Statement usesStrict local maximum

Proof usesNegation turns a strict local minimum into a strict local maximum · Strict second-derivative test, minimum version

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.