IsPositive — Mathlib

English

A linear operator T on a Hilbert space is called positive if it is symmetric and the real part of ⟪Tx, x⟫ is nonnegative for all x.

Русский

Линейный оператор T на гильбертовом пространстве называется положительным, если он симметричен и для каждого x выполняется Re ⟪Tx, x⟫ ≥ 0.

LaTeX

$$$T\\text{ is positive }\\quad\\Leftrightarrow\\quad (T\\text{ is symmetric}) \\land (\\forall x, 0 \\le \\Re\\\\langle Tx,x\\\\rangle).$$$

Lean4

/-- A linear operator `T` on a Hilbert space is **positive** if it is symmetric and
  `∀ x, 0 ≤ re ⟪T x, x⟫`. -/
def IsPositive (T : E →ₗ[𝕜] E) : Prop :=
  IsSymmetric T ∧ ∀ x, 0 ≤ re ⟪T x, x⟫

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