re_inner_nonneg_right — Mathlib

English

For a positive operator T and any x, the real part of the reverse inner product ⟪x, Tx⟫ is nonnegative.

Русский

Для положительного оператора T и любого x вещественная часть ⟪x, Tx⟫ неотрицательна.

LaTeX

$$$\\forall x, \\Re\\\\langle x,Tx\\\\rangle \\ge 0.$$$

Lean4

theorem re_inner_nonneg_right {T : E →ₗ[𝕜] E} (hT : IsPositive T) (x : E) : 0 ≤ re ⟪x, T x⟫ :=
  inner_re_symm (𝕜 := 𝕜) _ x ▸ hT.re_inner_nonneg_left x

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