Lagrange multipliers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
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.
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.
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.
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 Λ₀.
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 ℝ _