English
Let φ have a local extremum on the set {x | ∀ i, f_i(x) = f_i(x0)} at x0, and each f_i and φ be strictly differentiable at x0. Then there exist Λ ∈ ℝ^ι and Λ0 ∈ ℝ, not both zero, such that ∑_i Λ_i f_i′ + Λ0 φ′ = 0 as a linear functional on E.
Русский
Пусть φ имеет локальный экстремум на множество {x | ∀ i, f_i(x) = f_i(x0)} в x0, и все f_i, φ строго дифференциируемы в x0. Тогда существуют Λ ∈ ℝ^ι и Λ0 ∈ ℝ, не оба нули, такие что ∑ Λ_i f_i′ + Λ0 φ′ = 0 как линейный функционал на E.
LaTeX
$$$$\exists \Lambda : \mathbb{R}^{\i}, \exists \Lambda_0 \in \mathbb{R}, (\Lambda, \Lambda_0) \neq 0 \land \biggl( \sum_{i} \Lambda_i f_i' \biggr) + \Lambda_0 \phi' = 0.$$$$
Lean4
/-- Lagrange multipliers theorem: if `φ : E → ℝ` has a local extremum on the set `{x | f x = f x₀}`
at `x₀`, and both `f : E → ℝ` and `φ` are strictly differentiable at `x₀`, then there exist
`a b : ℝ` such that `(a, b) ≠ 0` and `a • f' + b • φ' = 0`. -/
theorem exists_multipliers_of_hasStrictFDerivAt_1d {f : E → ℝ} {f' : StrongDual ℝ E}
(hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀) (hf' : HasStrictFDerivAt f f' x₀) (hφ' : HasStrictFDerivAt φ φ' x₀) :
∃ a b : ℝ, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0 :=
by
obtain ⟨Λ, Λ₀, hΛ, hfΛ⟩ := hextr.exists_linear_map_of_hasStrictFDerivAt hf' hφ'
refine ⟨Λ 1, Λ₀, ?_, ?_⟩
· contrapose! hΛ
simp only [Prod.mk_eq_zero] at hΛ ⊢
refine ⟨LinearMap.ext fun x => ?_, hΛ.2⟩
simpa [hΛ.1] using Λ.map_smul x 1
· ext x
have H₁ : Λ (f' x) = f' x * Λ 1 := by simpa only [mul_one, Algebra.id.smul_eq_mul] using Λ.map_smul (f' x) 1
have H₂ : f' x * Λ 1 + Λ₀ * φ' x = 0 := by simpa only [Algebra.id.smul_eq_mul, H₁] using hfΛ x
simpa [mul_comm] using H₂
