Local extrema of differentiable functions

Main definitions

In a real normed space E we define posTangentConeAt (s : Set E) (x : E). This would be the same as tangentConeAt ℝ≥0 s x if we had a theory of normed semifields. This set is used in the proof of Fermat's Theorem (see below), and can be used to formalize Lagrange multipliers and/or Karush–Kuhn–Tucker conditions.

Main statements

For each theorem name listed below, we also prove similar theorems for min, extr (if applicable), and fderiv/deriv instead of HasFDerivAt/HasDerivAt.

• IsLocalMaxOn.hasFDerivWithinAt_nonpos : f' y ≤ 0 whenever a is a local maximum of f on s, f has derivative f' at a within s, and y belongs to the positive tangent cone of s at a.

• IsLocalMaxOn.hasFDerivWithinAt_eq_zero : In the settings of the previous theorem, if both y and -y belong to the positive tangent cone, then f' y = 0.

• IsLocalMax.hasFDerivAt_eq_zero : Fermat's Theorem, the derivative of a differentiable function at a local extremum point equals zero.

Implementation notes

For each mathematical fact we prove several versions of its formalization:

• for maxima and minima;
• using HasFDeriv*/HasDeriv* or fderiv*/deriv*.

For the fderiv*/deriv* versions we omit the differentiability condition whenever it is possible due to the fact that fderiv and deriv are defined to be zero for non-differentiable functions.

References

• Fermat's Theorem;
• Tangent cone;

Tags

local extremum, tangent cone, Fermat's Theorem

Positive tangent cone

def posTangentConeAt {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set E) (x : E) : Set E

"Positive" tangent cone to s at x; the only difference from tangentConeAt is that we require c n → ∞ instead of ‖c n‖ → ∞. One can think about posTangentConeAt as tangentConeAt NNReal but we have no theory of normed semifields yet.

theorem posTangentConeAt_mono {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : E} : Monotone fun (s : Set E) => posTangentConeAt s a

theorem mem_posTangentConeAt_of_frequently_mem {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x y : E} (h : ∃ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), x + t • y ∈ s) : y ∈ posTangentConeAt s x

theorem mem_posTangentConeAt_of_segment_subset {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x y : E} (h : segment ℝ x (x + y) ⊆ s) : y ∈ posTangentConeAt s x

If [x -[ℝ] x + y] ⊆ s, then y belongs to the positive tangent cone of s.

Before 2024-07-13, this lemma used to be called mem_posTangentConeAt_of_segment_subset. See also sub_mem_posTangentConeAt_of_segment_subset for the lemma that used to be called mem_posTangentConeAt_of_segment_subset.

theorem sub_mem_posTangentConeAt_of_segment_subset {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x y : E} (h : segment ℝ x y ⊆ s) : y - x ∈ posTangentConeAt s x

@[simp]

theorem posTangentConeAt_univ {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : E} : posTangentConeAt Set.univ a = Set.univ

Fermat's Theorem (vector space)

theorem IsLocalMaxOn.hasFDerivWithinAt_nonpos {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {s : Set E} {a y : E} (h : IsLocalMaxOn f s a) (hf : HasFDerivWithinAt f f' s a) (hy : y ∈ posTangentConeAt s a) : f' y ≤ 0

If f has a local max on s at a, f' is the derivative of f at a within s, and y belongs to the positive tangent cone of s at a, then f' y ≤ 0.

theorem IsLocalMaxOn.fderivWithin_nonpos {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a y : E} (h : IsLocalMaxOn f s a) (hy : y ∈ posTangentConeAt s a) : (fderivWithin ℝ f s a) y ≤ 0

If f has a local max on s at a and y belongs to the positive tangent cone of s at a, then f' y ≤ 0.

theorem IsLocalMaxOn.hasFDerivWithinAt_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {s : Set E} {a y : E} (h : IsLocalMaxOn f s a) (hf : HasFDerivWithinAt f f' s a) (hy : y ∈ posTangentConeAt s a) (hy' : -y ∈ posTangentConeAt s a) : f' y = 0

If f has a local max on s at a, f' is a derivative of f at a within s, and both y and -y belong to the positive tangent cone of s at a, then f' y ≤ 0.

theorem IsLocalMaxOn.fderivWithin_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a y : E} (h : IsLocalMaxOn f s a) (hy : y ∈ posTangentConeAt s a) (hy' : -y ∈ posTangentConeAt s a) : (fderivWithin ℝ f s a) y = 0

If f has a local max on s at a and both y and -y belong to the positive tangent cone of s at a, then f' y = 0.

theorem IsLocalMinOn.hasFDerivWithinAt_nonneg {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {s : Set E} {a y : E} (h : IsLocalMinOn f s a) (hf : HasFDerivWithinAt f f' s a) (hy : y ∈ posTangentConeAt s a) : 0 ≤ f' y

If f has a local min on s at a, f' is the derivative of f at a within s, and y belongs to the positive tangent cone of s at a, then 0 ≤ f' y.

theorem IsLocalMinOn.fderivWithin_nonneg {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a y : E} (h : IsLocalMinOn f s a) (hy : y ∈ posTangentConeAt s a) : 0 ≤ (fderivWithin ℝ f s a) y

If f has a local min on s at a and y belongs to the positive tangent cone of s at a, then 0 ≤ f' y.

theorem IsLocalMinOn.hasFDerivWithinAt_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {s : Set E} {a y : E} (h : IsLocalMinOn f s a) (hf : HasFDerivWithinAt f f' s a) (hy : y ∈ posTangentConeAt s a) (hy' : -y ∈ posTangentConeAt s a) : f' y = 0

If f has a local max on s at a, f' is a derivative of f at a within s, and both y and -y belong to the positive tangent cone of s at a, then f' y ≤ 0.

theorem IsLocalMinOn.fderivWithin_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a y : E} (h : IsLocalMinOn f s a) (hy : y ∈ posTangentConeAt s a) (hy' : -y ∈ posTangentConeAt s a) : (fderivWithin ℝ f s a) y = 0

If f has a local min on s at a and both y and -y belong to the positive tangent cone of s at a, then f' y = 0.

theorem IsLocalMin.hasFDerivAt_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {a : E} (h : IsLocalMin f a) (hf : HasFDerivAt f f' a) : f' = 0

Fermat's Theorem: the derivative of a function at a local minimum equals zero.

theorem IsLocalMin.fderiv_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} (h : IsLocalMin f a) : fderiv ℝ f a = 0

Fermat's Theorem: the derivative of a function at a local minimum equals zero.

theorem IsLocalMax.hasFDerivAt_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {a : E} (h : IsLocalMax f a) (hf : HasFDerivAt f f' a) : f' = 0

Fermat's Theorem: the derivative of a function at a local maximum equals zero.

theorem IsLocalMax.fderiv_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} (h : IsLocalMax f a) : fderiv ℝ f a = 0

Fermat's Theorem: the derivative of a function at a local maximum equals zero.

theorem IsLocalExtr.hasFDerivAt_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {a : E} (h : IsLocalExtr f a) : HasFDerivAt f f' a → f' = 0

Fermat's Theorem: the derivative of a function at a local extremum equals zero.

theorem IsLocalExtr.fderiv_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} (h : IsLocalExtr f a) : fderiv ℝ f a = 0

Fermat's Theorem: the derivative of a function at a local extremum equals zero.

Fermat's Theorem

theorem one_mem_posTangentConeAt_iff_mem_closure {s : Set ℝ} {a : ℝ} : 1 ∈ posTangentConeAt s a ↔ a ∈ closure (Set.Ioi a ∩ s)

theorem one_mem_posTangentConeAt_iff_frequently {s : Set ℝ} {a : ℝ} : 1 ∈ posTangentConeAt s a ↔ ∃ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), x ∈ s

theorem IsLocalMin.hasDerivAt_eq_zero {f : ℝ → ℝ} {f' a : ℝ} (h : IsLocalMin f a) (hf : HasDerivAt f f' a) : f' = 0

Fermat's Theorem: the derivative of a function at a local minimum equals zero.

theorem IsLocalMin.deriv_eq_zero {f : ℝ → ℝ} {a : ℝ} (h : IsLocalMin f a) : deriv f a = 0

Fermat's Theorem: the derivative of a function at a local minimum equals zero.

theorem IsLocalMax.hasDerivAt_eq_zero {f : ℝ → ℝ} {f' a : ℝ} (h : IsLocalMax f a) (hf : HasDerivAt f f' a) : f' = 0

Fermat's Theorem: the derivative of a function at a local maximum equals zero.

theorem IsLocalMax.deriv_eq_zero {f : ℝ → ℝ} {a : ℝ} (h : IsLocalMax f a) : deriv f a = 0

Fermat's Theorem: the derivative of a function at a local maximum equals zero.

theorem IsLocalExtr.hasDerivAt_eq_zero {f : ℝ → ℝ} {f' a : ℝ} (h : IsLocalExtr f a) : HasDerivAt f f' a → f' = 0

Fermat's Theorem: the derivative of a function at a local extremum equals zero.

theorem IsLocalExtr.deriv_eq_zero {f : ℝ → ℝ} {a : ℝ} (h : IsLocalExtr f a) : deriv f a = 0

Fermat's Theorem: the derivative of a function at a local extremum equals zero.