mathlib documentation

analysis.calculus.lagrange_multipliers

Lagrange multipliers #

In this file we formalize the Lagrange multipliers method of solving conditional extremum problems: if a function φ has a local extremum at x₀ on the set f ⁻¹' {f x₀}, f x = (f₀ x, ..., fₙ₋₁ x), then the differentials of fₖ and φ are linearly dependent. First we formulate a geometric version of this theorem which does not rely on the target space being ℝⁿ, then restate it in terms of coordinates.

TODO #

Formalize Karush-Kuhn-Tucker theorem

Tags #

lagrange multiplier, local extremum

theorem is_local_extr_on.range_ne_top_of_has_strict_fderiv_at {E : Type u_1} {F : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] [normed_add_comm_group F] [normed_space F] [complete_space F] {f : E → F} {φ : E → } {x₀ : E} {f' : E →L[] F} {φ' : E →L[] } (hextr : is_local_extr_on φ {x : E | f x = f x₀} x₀) (hf' : has_strict_fderiv_at f f' x₀) (hφ' : has_strict_fderiv_at φ φ' x₀) :
(f'.prod φ').range

Lagrange multipliers theorem: if φ : E → ℝ has a local extremum on the set {x | f x = f x₀} at x₀, both f : E → F and φ are strictly differentiable at x₀, and the codomain of f is a complete space, then the linear map x ↦ (f' x, φ' x) is not surjective.

theorem is_local_extr_on.exists_linear_map_of_has_strict_fderiv_at {E : Type u_1} {F : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] [normed_add_comm_group F] [normed_space F] [complete_space F] {f : E → F} {φ : E → } {x₀ : E} {f' : E →L[] F} {φ' : E →L[] } (hextr : is_local_extr_on φ {x : E | f x = f x₀} x₀) (hf' : has_strict_fderiv_at f f' x₀) (hφ' : has_strict_fderiv_at φ φ' x₀) :
∃ (Λ : module.dual F) (Λ₀ : ), (Λ, Λ₀) 0 ∀ (x : E), Λ (f' x) + Λ₀ φ' x = 0

Lagrange multipliers theorem: if φ : E → ℝ has a local extremum on the set {x | f x = f x₀} at x₀, both f : E → F and φ are strictly differentiable at x₀, and the codomain of f is a complete space, then there exist Λ : dual ℝ F and Λ₀ : ℝ such that (Λ, Λ₀) ≠ 0 and Λ (f' x) + Λ₀ • φ' x = 0 for all x.

theorem is_local_extr_on.exists_multipliers_of_has_strict_fderiv_at_1d {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {φ : E → } {x₀ : E} {φ' : E →L[] } {f : E → } {f' : E →L[] } (hextr : is_local_extr_on φ {x : E | f x = f x₀} x₀) (hf' : has_strict_fderiv_at f f' x₀) (hφ' : has_strict_fderiv_at φ φ' x₀) :
∃ (a b : ), (a, b) 0 a f' + b φ' = 0

Lagrange multipliers theorem: if φ : E → ℝ has a local extremum on the set {x | f x = f x₀} at x₀, and both f : E → ℝ and φ are strictly differentiable at x₀, then there exist a b : ℝ such that (a, b) ≠ 0 and a • f' + b • φ' = 0.

theorem is_local_extr_on.exists_multipliers_of_has_strict_fderiv_at {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {φ : E → } {x₀ : E} {φ' : E →L[] } {ι : Type u_2} [fintype ι] {f : ι → E → } {f' : ι → (E →L[] )} (hextr : is_local_extr_on φ {x : E | ∀ (i : ι), f i x = f i x₀} x₀) (hf' : ∀ (i : ι), has_strict_fderiv_at (f i) (f' i) x₀) (hφ' : has_strict_fderiv_at φ φ' x₀) :
∃ (Λ : ι → ) (Λ₀ : ), (Λ, Λ₀) 0 finset.univ.sum (λ (i : ι), Λ i f' i) + Λ₀ φ' = 0

Lagrange multipliers theorem, 1d version. Let f : ι → E → ℝ be a finite family of functions. Suppose that φ : E → ℝ has a local extremum on the set {x | ∀ i, f i x = f i x₀} at x₀. Suppose that all functions f i as well as φ are strictly differentiable at x₀. Then the derivatives f' i : E → L[ℝ] ℝ and φ' : E →L[ℝ] ℝ are linearly dependent: there exist Λ : ι → ℝ and Λ₀ : ℝ, (Λ, Λ₀) ≠ 0, such that ∑ i, Λ i • f' i + Λ₀ • φ' = 0.

See also is_local_extr_on.linear_dependent_of_has_strict_fderiv_at for a version that states ¬linear_independent ℝ _ instead of existence of Λ and Λ₀.

theorem is_local_extr_on.linear_dependent_of_has_strict_fderiv_at {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {φ : E → } {x₀ : E} {φ' : E →L[] } {ι : Type u_2} [finite ι] {f : ι → E → } {f' : ι → (E →L[] )} (hextr : is_local_extr_on φ {x : E | ∀ (i : ι), f i x = f i x₀} x₀) (hf' : ∀ (i : ι), has_strict_fderiv_at (f i) (f' i) x₀) (hφ' : has_strict_fderiv_at φ φ' x₀) :

Lagrange multipliers theorem. Let f : ι → E → ℝ be a finite family of functions. Suppose that φ : E → ℝ has a local extremum on the set {x | ∀ i, f i x = f i x₀} at x₀. Suppose that all functions f i as well as φ are strictly differentiable at x₀. Then the derivatives f' i : E → L[ℝ] ℝ and φ' : E →L[ℝ] ℝ are linearly dependent.

See also is_local_extr_on.exists_multipliers_of_has_strict_fderiv_at for a version that that states existence of Lagrange multipliers Λ and Λ₀ instead of using ¬linear_independent ℝ _