English
If hextr is a local extremum for a self-adjoint operator, then T x0 equals the Rayleigh quotient times x0 (in appropriate scalars).
Русский
Если x0 является локальным экстремумом для самосопряжённого оператора, тогда T x0 равно коэффициенту Райли, умноженному на x0.
LaTeX
$$$T x_0 = (\\text{RayleighQuotient}_T(x_0))\\, x_0$ (interpreted in the base field).$$
Lean4
theorem eq_smul_self_of_isLocalExtrOn_real (hT : IsSelfAdjoint T) {x₀ : F}
(hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : F) ‖x₀‖) x₀) : T x₀ = T.rayleighQuotient x₀ • x₀ :=
by
obtain ⟨a, b, h₁, h₂⟩ := hT.linearly_dependent_of_isLocalExtrOn hextr
by_cases hx₀ : x₀ = 0
· simp [hx₀]
by_cases hb : b = 0
· have : a ≠ 0 := by simpa [hb] using h₁
refine absurd ?_ hx₀
apply smul_right_injective F this
simpa [hb] using h₂
let c : ℝ := -b⁻¹ * a
have hc : T x₀ = c • x₀ := by
have : b * (b⁻¹ * a) = a := by field_simp
apply smul_right_injective F hb
simp [c, eq_neg_of_add_eq_zero_left h₂, ← mul_smul, this]
convert hc
have := congr_arg (fun x => ⟪x, x₀⟫_ℝ) hc
simp [field, inner_smul_left, real_inner_self_eq_norm_mul_norm, mul_comm a] at this ⊢
exact this
