Theorems · Theorem · optimization

IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {φ : E → ℝ} {x₀ : E}
  {φ' : StrongDual ℝ E} {ι : Type u_3} [Finite ι] {f : ι → E → ℝ} {f' : ι → StrongDual ℝ E},
  IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀ →
    (∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀) →
      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 φ' : StrongDual ℝ E 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 ℝ _

Defined in

Mathlib.Analysis.Calculus.LagrangeMultipliers

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceFinite