image_rayleigh_eq_image_rayleigh_sphere

English

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

Русский

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

LaTeX

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

Lean4

theorem image_rayleigh_eq_image_rayleigh_sphere {r : ℝ} (hr : 0 < r) :
    rayleighQuotient T '' {0}ᶜ = rayleighQuotient T '' sphere 0 r :=
  by
  ext a
  constructor
  · rintro ⟨x, hx : x ≠ 0, hxT⟩
    let c : 𝕜 := ↑‖x‖⁻¹ * r
    have : c ≠ 0 := by simp [c, hx, hr.ne']
    refine ⟨c • x, ?_, ?_⟩
    · simp [field, c, norm_smul, abs_of_pos hr]
    · rw [T.rayleigh_smul x this]
      exact hxT
  · rintro ⟨x, hx, hxT⟩
    exact ⟨x, ne_zero_of_mem_sphere hr.ne' ⟨x, hx⟩, hxT⟩

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