re_inner_adjoint_mul_self_nonneg — Mathlib

English

For all x, the real part of ⟪x, T†T x⟫ is nonnegative.

Русский

Для любого x действительная часть ⟪x, T†T x⟫ неотрицательна.

LaTeX

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

Lean4

/-- The Gram operator T†T is a positive operator. -/
theorem re_inner_adjoint_mul_self_nonneg (T : E →ₗ[𝕜] E) (x : E) : 0 ≤ re ⟪x, (T.adjoint * T) x⟫ :=
  by
  simp only [Module.End.mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K]
  norm_cast
  exact sq_nonneg _

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