# Documentation

Mathlib.Analysis.Calculus.LagrangeMultipliers

# 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 IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAt {E : Type u_1} {F : Type u_2} [] [] [] [] {f : EF} {φ : E} {x₀ : E} {f' : E →L[] F} {φ' : } (hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀) (hf' : HasStrictFDerivAt f f' x₀) (hφ' : HasStrictFDerivAt φ φ' x₀) :

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 IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt {E : Type u_1} {F : Type u_2} [] [] [] [] {f : EF} {φ : E} {x₀ : E} {f' : E →L[] F} {φ' : } (hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀) (hf' : HasStrictFDerivAt f f' x₀) (hφ' : HasStrictFDerivAt φ φ' x₀) :
Λ Λ₀, (Λ, Λ₀) 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 IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d {E : Type u_1} [] [] {φ : E} {x₀ : E} {φ' : } {f : E} {f' : } (hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀) (hf' : HasStrictFDerivAt f f' x₀) (hφ' : HasStrictFDerivAt φ φ' 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 IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt {E : Type u_1} [] [] {φ : E} {x₀ : E} {φ' : } {ι : Type u_3} [] {f : ιE} {f' : ι} (hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀) (hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀) (hφ' : HasStrictFDerivAt φ φ' x₀) :
Λ Λ₀, (Λ, Λ₀) 0 (Finset.sum Finset.univ fun 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 IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt for a version that states ¬LinearIndependent ℝ _ instead of existence of Λ and Λ₀.

theorem IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt {E : Type u_1} [] [] {φ : E} {x₀ : E} {φ' : } {ι : Type u_3} [] {f : ιE} {f' : ι} (hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀) (hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀) (hφ' : HasStrictFDerivAt φ φ' 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 IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt for a version that that states existence of Lagrange multipliers Λ and Λ₀ instead of using ¬LinearIndependent ℝ _