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} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {φ : E → ℝ} {x₀ : E} {f' : E →L[ℝ] F} {φ' : E →L[ℝ] ℝ} (hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀) (hf' : HasStrictFDerivAt f f' x₀) (hφ' : HasStrictFDerivAt φ φ' x₀) : LinearMap.range (ContinuousLinearMap.prod f' φ') ≠ ⊤

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} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {φ : E → ℝ} {x₀ : E} {f' : E →L[ℝ] F} {φ' : E →L[ℝ] ℝ} (hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀) (hf' : HasStrictFDerivAt f f' x₀) (hφ' : HasStrictFDerivAt φ φ' 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 IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {φ : E → ℝ} {x₀ : E} {φ' : E →L[ℝ] ℝ} {f : E → ℝ} {f' : E →L[ℝ] ℝ} (hextr : IsLocalExtrOn φ {x : E | 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} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {φ : E → ℝ} {x₀ : E} {φ' : E →L[ℝ] ℝ} {ι : Type u_3} [Fintype ι] {f : ι → E → ℝ} {f' : ι → E →L[ℝ] ℝ} (hextr : IsLocalExtrOn φ {x : E | ∀ (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} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {φ : E → ℝ} {x₀ : E} {φ' : E →L[ℝ] ℝ} {ι : Type u_3} [Finite ι] {f : ι → E → ℝ} {f' : ι → E →L[ℝ] ℝ} (hextr : IsLocalExtrOn φ {x : E | ∀ (i : ι), f i x = f i x₀} x₀) (hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀) (hφ' : HasStrictFDerivAt φ φ' x₀) : ¬LinearIndependent ℝ (Option.elim' φ' f')

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 ℝ _