English
If φ has a local extremum on the set {x ∈ E | f(x) = f(x0)} at x0, and both f and φ are strictly differentiable at x0, and the codomain of f is a complete space, then there exist Λ ∈ dual(F) and Λ0 ∈ R with (Λ, Λ0) ≠ 0 such that Λ(f′) + Λ0 φ′ = 0 on E.
Русский
Пусть φ имеет локальный экстремум на множествах {x ∈ E | f(x) = f(x0)} в точке x0, при этом f и φ строго дифференцируемы в x0, и область значений f полнота; тогда существуют Λ ∈ двойственному пространству F и Λ0 ∈ R такие, что (Λ, Λ0) ≠ 0 и Λ∘f′ + Λ0 φ′ = 0 как функционал на E.
LaTeX
$$$$\exists \Lambda \in (F \to\_ℝ \mathbb{R}) , \exists \Lambda_0 \in \mathbb{R}, (\Lambda, \Lambda_0) \neq 0 \land (\Lambda \circ f' ) + \Lambda_0 \circ φ' = 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 the linear map `x ↦ (f' x, φ' x)` is not surjective. -/
theorem range_ne_top_of_hasStrictFDerivAt (hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀)
(hf' : HasStrictFDerivAt f f' x₀) (hφ' : HasStrictFDerivAt φ φ' x₀) : LinearMap.range (f'.prod φ') ≠ ⊤ :=
by
intro htop
set fφ := fun x => (f x, φ x)
have A : map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀) :=
by
change map (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p | p.1 = f x₀}] x₀) = 𝓝 (φ x₀)
rw [← map_map, nhdsWithin, map_inf_principal_preimage, (hf'.prodMk hφ').map_nhds_eq_of_surj htop]
exact map_snd_nhdsWithin _
exact hextr.not_nhds_le_map A.ge
