# mathlibdocumentation

analysis.calculus.local_extr

# 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 ≤ 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.

• is_local_max_on.has_fderiv_within_at_eq_zero : In the settings of the previous theorem, if both y and -y belong to the positive tangent cone, then f' 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 function f continuous on [a, b] and differentiable on (a, b), there exists c ∈ (a, b) such that f' c = 0.

## Implementation notes #

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

• for maxima and minima;
• using has_fderiv*/has_deriv* 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.

## Tags #

local extremum, Fermat's Theorem, Rolle's Theorem