iSup_rayleigh_eq_iSup_rayleigh_sphere

English

The infimum of the Rayleigh quotient over all nonzero vectors equals the infimum over the sphere of radius r.

Русский

Нижняя грань коэффициента Райли по всем ненулевым векторам равна нижней грани по сфере радиуса r.

LaTeX

$$$\\inf_{x\\neq0} \\rho_T(x) = \\inf_{\\|x\\|=r} \\rho_T(x).$$$

Lean4

theorem iSup_rayleigh_eq_iSup_rayleigh_sphere {r : ℝ} (hr : 0 < r) :
    ⨆ x : { x : E // x ≠ 0 }, rayleighQuotient T x = ⨆ x : sphere (0 : E) r, rayleighQuotient T x :=
  show ⨆ x : ({0}ᶜ : Set E), rayleighQuotient T x = _ by
    simp only [← @sSup_image' _ _ _ _ (rayleighQuotient T), T.image_rayleigh_eq_image_rayleigh_sphere hr]

Похожие утверждения