Theorems · Theorem · optimization

IsLocalExtrOn.range_ne_top_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₀ → (↑(f'.prod φ')).range ≠ ⊤

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.

Defined in

Mathlib.Analysis.Calculus.LagrangeMultipliers

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceCompleteSpace