English
Let f be a finite family of real-valued functions on E and φ a real-valued function, as above. Then there exists a nontrivial linear relation among the derivatives f_i′ and φ′ at x0, expressed as Λ_i f_i′ + Λ0 φ′ = 0 for all i.
Русский
Пусть есть конечная система функций f_i и функция φ, как выше, тогда существует ненулевой набор коэффициентов Λ_i и Λ0, удовлетворяющий линейной зависимости между производными f_i′ и φ′: сумма Λ_i f_i′ плюс Λ0 φ′ равна нулю на E.
LaTeX
$$$$\exists (\Lambda : \mathbb{R}^{\i}), \exists \Lambda_0 \in \mathbb{R}, (\Lambda, \Lambda_0) \neq 0 \land \sum_i \Lambda_i f_i' + \Lambda_0 φ' = 0.$$$$
Lean4
/-- 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 `φ' : StrongDual ℝ E` are linearly dependent:
there exist `Λ : ι → ℝ` and `Λ₀ : ℝ`, `(Λ, Λ₀) ≠ 0`, such that `∑ i, Λ i • f' i + Λ₀ • φ' = 0`.
See also `IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt` for a version that
states `¬LinearIndependent ℝ _` instead of existence of `Λ` and `Λ₀`. -/
theorem exists_multipliers_of_hasStrictFDerivAt {ι : Type*} [Fintype ι] {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₀) : ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ (∑ i, Λ i • f' i) + Λ₀ • φ' = 0 :=
by
letI := Classical.decEq ι
replace hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀ := by simpa only [funext_iff] using hextr
rcases hextr.exists_linear_map_of_hasStrictFDerivAt (hasStrictFDerivAt_pi.2 fun i => hf' i) hφ' with ⟨Λ, Λ₀, h0, hsum⟩
rcases (LinearEquiv.piRing ℝ ℝ ι ℝ).symm.surjective Λ with ⟨Λ, rfl⟩
refine ⟨Λ, Λ₀, ?_, ?_⟩
· simpa only [Ne, Prod.ext_iff, LinearEquiv.map_eq_zero_iff, Prod.fst_zero] using h0
· ext x; simpa [mul_comm] using hsum x
