adjointAux_norm — Mathlib

English

The norm of A x equals the square root of the real part of the inner product ⟪(A† A)x, x⟫.

Русский

Модуль ||A x|| равен корню квадратному из вещественной части скобки ⟪(A†A)x, x⟫.

LaTeX

$$$$ \\|A x\\| = \\sqrt{\\mathrm{Re} \\langle (A^{\\dagger} \\circ A) x, x \\rangle}. $$$$

Lean4

@[simp]
theorem adjointAux_norm (A : E →L[𝕜] F) : ‖adjointAux A‖ = ‖A‖ :=
  by
  refine le_antisymm ?_ ?_
  · refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_
    rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
    exact toSesqForm_apply_norm_le
  · nth_rw 1 [← adjointAux_adjointAux A]
    refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_
    rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
    exact toSesqForm_apply_norm_le

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