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