isPositive_iff — Mathlib

English

For a continuous linear map T on a complex inner product space, IsPositive T holds if and only if T is self-adjoint and ⟪Tx, x⟫ ≥ 0 for all x.

Русский

Для непрерывного линейного отображения T на комплексном векторном пространстве с скалярным произведением верно: IsPositive T тогда и только тогда, когда T — самосопряжённый и для всех x выполняется ⟪Tx, x⟫ ≥ 0.

LaTeX

$$$\text{IsPositive } T \iff \text{IsSelfAdjoint } T \ \wedge\ \forall x\, (0 \le \langle T x, x \rangle).$$$

Lean4

theorem isPositive_iff (T : E →L[𝕜] E) : IsPositive T ↔ IsSelfAdjoint T ∧ ∀ x, 0 ≤ ⟪T x, x⟫ := by
  simp [← isPositive_toLinearMap_iff, isSelfAdjoint_iff_isSymmetric, LinearMap.isPositive_iff]

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