re_inner_nonneg_left

Mathlib.Analysis.InnerProductSpace.Positive

URI: https://scilib.ai/kg/mathlib#LinearMap.IsPositive.re_inner_nonneg_left

English

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

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru