English
Under the hypotheses for a finite ι and strict differentiability of all f_i and φ at x0, the family {f_i′} together with φ′ is linearly dependent; i.e., there exist Λ_i and Λ0, not all zero, with ∑ Λ_i f_i′ + Λ0 φ′ = 0.
Русский
При тех же предположениях для конечной множества индексов ι и строгой дифференциации всех f_i и φ в x0, производные f_i′ и φ′ линейно зависимы: существуют коэффициенты Λ_i и Λ0, не все нулевые, удовлетворяющие равенству ∑ Λ_i f_i′ + Λ0 φ′ = 0.
LaTeX
$$$$\exists (\Lambda : \mathbb{R}^{\i}) (\Lambda_0 : \mathbb{R}), (\Lambda, Λ_0) \neq 0 \land \bigl( \sum_i Λ_i f_i' \bigr) + Λ_0 φ' = 0.$$$$
Lean4
/-- 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 ℝ _` -/
theorem linear_dependent_of_hasStrictFDerivAt {ι : Type*} [Finite ι] {f : ι → E → ℝ} {f' : ι → StrongDual ℝ E}
(hextr : IsLocalExtrOn φ {x | ∀ i, f i x = f i x₀} x₀) (hf' : ∀ i, HasStrictFDerivAt (f i) (f' i) x₀)
(hφ' : HasStrictFDerivAt φ φ' x₀) : ¬LinearIndependent ℝ (Option.elim' φ' f' : Option ι → StrongDual ℝ E) :=
by
cases nonempty_fintype ι
rw [Fintype.linearIndependent_iff]; push_neg
rcases hextr.exists_multipliers_of_hasStrictFDerivAt hf' hφ' with ⟨Λ, Λ₀, hΛ, hΛf⟩
refine ⟨Option.elim' Λ₀ Λ, ?_, ?_⟩
· simpa [add_comm] using hΛf
· simpa only [funext_iff, not_and_or, or_comm, Option.exists, Prod.mk_eq_zero, Ne, not_forall] using hΛ
