English
If hextr is a local extremum of T.reApplyInnerSelf on a sphere and the extremum is real, then x0 is an eigenvector of T with eigenvalue equal to the Rayleigh quotient.
Русский
Если точка x0 является локальным экстремумом функционала T.reApplyInnerSelf на сфере и соответствующий предел реален, то x0 является собственным вектором T с собственным значением, равным коэффициенту Райли.
LaTeX
$$$T x_0 = (\\operatorname{RayleighQuotient}_T(x_0))\\, x_0$.$$
Lean4
theorem linearly_dependent_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : F}
(hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : F) ‖x₀‖) x₀) :
∃ a b : ℝ, (a, b) ≠ 0 ∧ a • x₀ + b • T x₀ = 0 :=
by
have H : IsLocalExtrOn T.reApplyInnerSelf {x : F | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀ :=
by
convert hextr
ext x
simp
-- find Lagrange multipliers for the function `T.re_apply_inner_self` and the
-- hypersurface-defining function `fun x ↦ ‖x‖ ^ 2`
obtain ⟨a, b, h₁, h₂⟩ :=
IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d H (hasStrictFDerivAt_norm_sq x₀)
(hT.isSymmetric.hasStrictFDerivAt_reApplyInnerSelf x₀)
refine ⟨a, b, h₁, ?_⟩
apply (InnerProductSpace.toDualMap ℝ F).injective
simp only [LinearIsometry.map_add, LinearIsometry.map_zero]
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `map_smulₛₗ` into `map_smulₛₗ _`
simp only [map_smulₛₗ _, RCLike.conj_to_real]
change a • innerSL ℝ x₀ + b • innerSL ℝ (T x₀) = 0
apply smul_right_injective (F →L[ℝ] ℝ) (two_ne_zero : (2 : ℝ) ≠ 0)
simpa only [two_smul, smul_add, add_smul, add_zero] using h₂
