mathlib documentation

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`.

Implementation notes #

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

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

def pos_tangent_cone_at {E : Type u} [normed_add_comm_group E] [normed_space E] (s : set E) (x : E) :
set E

"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
theorem pos_tangent_cone_at_mono {E : Type u} [normed_add_comm_group E] [normed_space E] {a : E} :
monotone (λ (s : set E), pos_tangent_cone_at s a)
theorem mem_pos_tangent_cone_at_of_segment_subset {E : Type u} [normed_add_comm_group E] [normed_space E] {s : set E} {x y : E} (h : segment x y s) :
theorem mem_pos_tangent_cone_at_of_segment_subset' {E : Type u} [normed_add_comm_group E] [normed_space E] {s : set E} {x y : E} (h : segment x (x + y) s) :
theorem is_local_max_on.has_fderiv_within_at_nonpos {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {f' : E →L[] } {s : set E} (h : is_local_max_on f s a) (hf : has_fderiv_within_at f f' s a) {y : E} (hy : y pos_tangent_cone_at 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 is_local_max_on.fderiv_within_nonpos {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {s : set E} (h : is_local_max_on f s a) {y : E} (hy : y pos_tangent_cone_at s a) :

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 is_local_max_on.has_fderiv_within_at_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {f' : E →L[] } {s : set E} (h : is_local_max_on f s a) (hf : has_fderiv_within_at f f' s a) {y : E} (hy : y pos_tangent_cone_at s a) (hy' : -y pos_tangent_cone_at 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 is_local_max_on.fderiv_within_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {s : set E} (h : is_local_max_on f s a) {y : E} (hy : y pos_tangent_cone_at s a) (hy' : -y pos_tangent_cone_at s a) :
(fderiv_within 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 is_local_min_on.has_fderiv_within_at_nonneg {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {f' : E →L[] } {s : set E} (h : is_local_min_on f s a) (hf : has_fderiv_within_at f f' s a) {y : E} (hy : y pos_tangent_cone_at 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 is_local_min_on.fderiv_within_nonneg {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {s : set E} (h : is_local_min_on f s a) {y : E} (hy : y pos_tangent_cone_at s a) :

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 is_local_min_on.has_fderiv_within_at_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {f' : E →L[] } {s : set E} (h : is_local_min_on f s a) (hf : has_fderiv_within_at f f' s a) {y : E} (hy : y pos_tangent_cone_at s a) (hy' : -y pos_tangent_cone_at 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 is_local_min_on.fderiv_within_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {s : set E} (h : is_local_min_on f s a) {y : E} (hy : y pos_tangent_cone_at s a) (hy' : -y pos_tangent_cone_at s a) :
(fderiv_within 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 is_local_min.has_fderiv_at_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {f' : E →L[] } (h : is_local_min f a) (hf : has_fderiv_at f f' a) :
f' = 0

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

theorem is_local_min.fderiv_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} (h : is_local_min f a) :
fderiv f a = 0

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

theorem is_local_max.has_fderiv_at_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {f' : E →L[] } (h : is_local_max f a) (hf : has_fderiv_at f f' a) :
f' = 0

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

theorem is_local_max.fderiv_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} (h : is_local_max f a) :
fderiv f a = 0

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

theorem is_local_extr.has_fderiv_at_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} {f' : E →L[] } (h : is_local_extr f a) :
has_fderiv_at f f' af' = 0

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

theorem is_local_extr.fderiv_eq_zero {E : Type u} [normed_add_comm_group E] [normed_space E] {f : E → } {a : E} (h : is_local_extr f a) :
fderiv f a = 0

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

theorem is_local_min.has_deriv_at_eq_zero {f : } {f' a : } (h : is_local_min f a) (hf : has_deriv_at f f' a) :
f' = 0

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

theorem is_local_min.deriv_eq_zero {f : } {a : } (h : is_local_min f a) :
deriv f a = 0

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

theorem is_local_max.has_deriv_at_eq_zero {f : } {f' a : } (h : is_local_max f a) (hf : has_deriv_at f f' a) :
f' = 0

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

theorem is_local_max.deriv_eq_zero {f : } {a : } (h : is_local_max f a) :
deriv f a = 0

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

theorem is_local_extr.has_deriv_at_eq_zero {f : } {f' a : } (h : is_local_extr f a) :
has_deriv_at f f' af' = 0

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

theorem is_local_extr.deriv_eq_zero {f : } {a : } (h : is_local_extr f a) :
deriv f a = 0

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

theorem exists_Ioo_extr_on_Icc (f : ) {a b : } (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hfI : f a = f b) :
∃ (c : ) (H : c set.Ioo a b), is_extr_on f (set.Icc a b) c

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.

theorem exists_local_extr_Ioo (f : ) {a b : } (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hfI : f a = f b) :
∃ (c : ) (H : c set.Ioo a b), is_local_extr f c

A continuous function on a closed interval with f a = f b has a local extremum at some point of the corresponding open interval.

theorem exists_has_deriv_at_eq_zero (f f' : ) {a b : } (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hfI : f a = f b) (hff' : ∀ (x : ), x set.Ioo a bhas_deriv_at f (f' x) x) :
∃ (c : ) (H : c set.Ioo a b), f' c = 0

Rolle's Theorem has_deriv_at version

theorem exists_deriv_eq_zero (f : ) {a b : } (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hfI : f a = f b) :
∃ (c : ) (H : c set.Ioo a b), deriv f c = 0

Rolle's Theorem deriv version

theorem exists_has_deriv_at_eq_zero' {f f' : } {a b l : } (hab : a < b) (hfa : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds l)) (hfb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds l)) (hff' : ∀ (x : ), x set.Ioo a bhas_deriv_at f (f' x) x) :
∃ (c : ) (H : c set.Ioo a b), f' c = 0

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).

theorem exists_deriv_eq_zero' {f : } {a b l : } (hab : a < b) (hfa : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds l)) (hfb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds l)) :
∃ (c : ) (H : c set.Ioo a b), deriv f c = 0

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.