Local extrema of smooth functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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, a version for a function on an open interval: if f has derivative f'
on (a, b) and has the same limit l at 𝓝[>] a and 𝓝[<] b, then f' c = 0
for some c ∈ (a, b).
Rolle's Theorem, a version for a function on an open interval: if f has the same limit
l at 𝓝[>] a and 𝓝[<] b, then deriv f c = 0 for some c ∈ (a, b). This version
does not require differentiability of f because we define deriv f c = 0 whenever f is not
differentiable at c.
The number of roots of a real polynomial p is at most the number of roots of its derivative
that are not roots of p plus one.
The number of roots of a real polynomial is at most the number of roots of its derivative plus one.
The number of roots of a real polynomial (counted with multiplicities) is at most the number of roots of its derivative (counted with multiplicities) plus one.
The number of real roots of a polynomial is at most the number of roots of its derivative plus one.