apply_norm_sq_eq_inner_adjoint_right

English

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

Русский

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

LaTeX

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

Lean4

theorem apply_norm_sq_eq_inner_adjoint_right (A : E →L[𝕜] F) (x : E) : ‖A x‖ ^ 2 = re ⟪x, (A† ∘L A) x⟫ :=
  by
  have h : ⟪x, (A† ∘L A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]; rfl
  rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

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