isSymmetric_adjoint_mul_self — Mathlib

English

The Gram operator T†T is a positive operator: ⟨x, (T†T) x⟩ ≥ 0 for all x.

Русский

Грамов оператор T†T является положительным: для всех x выполнено ⟨x, (T†T) x⟩ ≥ 0.

LaTeX

$$$$\langle x, (T^{*}T) x\rangle \ge 0 \quad\text{for all } x.$$$$

Lean4

/-- The Gram operator T†T is symmetric. -/
theorem isSymmetric_adjoint_mul_self (T : E →ₗ[𝕜] E) : IsSymmetric (T.adjoint * T) :=
  by
  intro x y
  simp [adjoint_inner_left, adjoint_inner_right]

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