iInf_rayleigh_eq_iInf_rayleigh_sphere

English

The same infimum equality as above for the Rayleigh quotient on a sphere of radius r.

Русский

Та же равенство инфимума коэффициента Райли на сфере радиуса r.

LaTeX

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

Lean4

theorem iInf_rayleigh_eq_iInf_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 [← @sInf_image' _ _ _ _ (rayleighQuotient T), T.image_rayleigh_eq_image_rayleigh_sphere hr]

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