English
In the 1-dimensional setting, if φ has a local extremum on {x ∈ E | f(x) = f(x0)} at x0, and f and φ are strictly differentiable at x0, then there exist a,b ∈ R, not both zero, such that a f′ + b φ′ = 0 as functionals on E.
Русский
В одномерном случае для локального экстремума φ на множестве {x | f(x) = f(x0)} в точке x0 существует пара множителей a,b ∈ R, не обе равны нулю, такая что a f′ + b φ′ = 0 как линейные функционалы на E.
LaTeX
$$$$\exists a,b \in \mathbb{R}, \ (a,b) \neq (0,0) \land a f' + b φ' = 0.$$$$
Lean4
/-- 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 there exist `Λ : dual ℝ F` and `Λ₀ : ℝ` such that `(Λ, Λ₀) ≠ 0` and
`Λ (f' x) + Λ₀ • φ' x = 0` for all `x`. -/
theorem exists_linear_map_of_hasStrictFDerivAt (hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀)
(hf' : HasStrictFDerivAt f f' x₀) (hφ' : HasStrictFDerivAt φ φ' x₀) :
∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∀ x, Λ (f' x) + Λ₀ • φ' x = 0 :=
by
rcases
Submodule.exists_le_ker_of_lt_top _ (lt_top_iff_ne_top.2 <| hextr.range_ne_top_of_hasStrictFDerivAt hf' hφ') with
⟨Λ', h0, hΛ'⟩
set e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
((LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prodCongr (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm).trans
(LinearMap.coprodEquiv ℝ)
rcases e.surjective Λ' with ⟨⟨Λ, Λ₀⟩, rfl⟩
refine ⟨Λ, Λ₀, e.map_ne_zero_iff.1 h0, fun x => ?_⟩
convert LinearMap.congr_fun (LinearMap.range_le_ker_iff.1 hΛ') x using 1
-- squeezed `simp [mul_comm]` to speed up elaboration
simp only [e, smul_eq_mul, LinearEquiv.trans_apply, LinearEquiv.prodCongr_apply, LinearEquiv.refl_apply,
LinearMap.ringLmapEquivSelf_symm_apply, LinearMap.coprodEquiv_apply, ContinuousLinearMap.coe_prod,
LinearMap.coprod_comp_prod, LinearMap.add_apply, LinearMap.coe_comp, ContinuousLinearMap.coe_coe,
Function.comp_apply, LinearMap.coe_smulRight, Module.End.one_apply, mul_comm]
