Local extrema of smooth functions
Main definitions
In a real normed space E we define pos_tangent_cone_at (s : set E) (x : E).
This would be the same as tangent_cone_at ℝ≥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(f)derivinstead ofhas_fderiv`.
is_local_max_on.has_fderiv_within_at_nonpos:f' y ≤ 0wheneverais a local maximum offons,fhas derivativef'atawithins, andybelongs to the positive tangent cone ofsata.is_local_max_on.has_fderiv_within_at_eq_zero: In the settings of the previous theorem, if bothyand-ybelong to the positive tangent cone, thenf' y = 0.is_local_max.has_fderiv_at_eq_zero: Fermat's Theorem, the derivative of a differentiable function at a local extremum point equals zero.exists_has_deriv_at_eq_zero: Rolle's Theorem: given a functionfcontinuous on[a, b]and differentiable on(a, b), there existsc ∈ (a, b)such thatf' c = 0.
Implementation notes
For each mathematical fact we prove several versions of its formalization:
- for maxima and minima;
- using
has_fderiv*/has_deriv*orfderiv*/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
Tags
local extremum, Fermat's Theorem, Rolle's Theorem
"Positive" tangent cone to s at x; the only difference from tangent_cone_at
is that we require c n → ∞ instead of ∥c n∥ → ∞. One can think about pos_tangent_cone_at
as tangent_cone_at nnreal but we have no theory of normed semifields yet.
Equations
- pos_tangent_cone_at s x = {y : E | ∃ (c : ℕ → ℝ) (d : ℕ → E), (∀ᶠ (n : ℕ) in filter.at_top, x + d n ∈ s) ∧ filter.tendsto c filter.at_top filter.at_top ∧ filter.tendsto (λ (n : ℕ), c n • d n) filter.at_top (nhds y)}
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.
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.
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.
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.
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.
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.
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.
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.
Fermat's Theorem: the derivative of a function at a local minimum equals zero.
Fermat's Theorem: the derivative of a function at a local minimum equals zero.
Fermat's Theorem: the derivative of a function at a local maximum equals zero.
Fermat's Theorem: the derivative of a function at a local maximum equals zero.
Fermat's Theorem: the derivative of a function at a local extremum equals zero.
Fermat's Theorem: the derivative of a function at a local extremum equals zero.
Fermat's Theorem: the derivative of a function at a local minimum equals zero.
Fermat's Theorem: the derivative of a function at a local minimum equals zero.
Fermat's Theorem: the derivative of a function at a local maximum equals zero.
Fermat's Theorem: the derivative of a function at a local maximum equals zero.
Fermat's Theorem: the derivative of a function at a local extremum equals zero.
Fermat's Theorem: the derivative of a function at a local extremum equals zero.
A continuous function on a closed interval with f a = f b takes either its maximum
or its minimum value at a point in the interior of the interval.
A continuous function on a closed interval with f a = f b has a local extremum at some
point of the corresponding open interval.
Rolle's Theorem has_deriv_at version