Theorems · Theorem · optimization

IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {φ : E → ℝ} {x₀ : E}
  {f' : E →L[ℝ] F} {φ' : StrongDual ℝ E},
  IsLocalExtrOn φ {x | f x = f x₀} x₀ →
    HasStrictFDerivAt f f' x₀ → 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.

Defined in

Mathlib.Analysis.Calculus.LagrangeMultipliers

Cited by

2 results in Mathlib

Foundations

Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceCompleteSpace