rayleigh_smul — Mathlib

English

For r>0, the images of the Rayleigh quotient on {0}^c and on the sphere of radius r are equal.

Русский

Для $r>0$ образы коэффициента Райли на множестве $\\{0\\}^c$ и на сфере радиуса $r$ совпадают.

LaTeX

$$$\\rho_T''(\\{0\\}^c) = \\rho_T''(\\mathbb{S}(0,r)).$$$

Lean4

theorem rayleigh_smul (x : E) {c : 𝕜} (hc : c ≠ 0) : rayleighQuotient T (c • x) = rayleighQuotient T x :=
  by
  by_cases hx : x = 0
  · simp [hx]
  simp [field, norm_smul, T.reApplyInnerSelf_smul]

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