isPositive_iff — Mathlib

English

For a linear map T on a complex inner product space, T is positive if and only if T is symmetric and ⟪Tx, x⟫ ≥ 0 for all x.

Русский

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

LaTeX

$$$$\mathrm{IsPositive}(T) \;\iff\; (\mathrm{IsSymmetric}(T) \land \forall x, \; 0 \le \langle Tx, x \rangle).$$$$

Lean4

theorem isPositive_iff (T : E →ₗ[𝕜] E) : IsPositive T ↔ IsSymmetric T ∧ ∀ x, 0 ≤ ⟪T x, x⟫ :=
  by
  simp_rw [IsPositive, and_congr_right_iff, ← RCLike.ofReal_nonneg (K := 𝕜)]
  intro hT
  simp [hT]

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