isPositive_iff_complex — Mathlib

English

For a complex-linear operator T, T is positive if and only if for all x the inner product ⟪Tx, x⟫ is real and nonnegative.

Русский

Для комплексного линейного оператора T: T положителен тогда и только тогда, когда для всех x скалярное произведение ⟪Tx, x⟫ реально и неотрицательно.

LaTeX

$$$T \\text{ is positive} \\iff \\forall x,\\; \\Im(\\\\langle Tx,x\\\\rangle_\\mathbb{C})=0 \\land \\Re(\\\\langle Tx,x\\\\rangle_\\mathbb{C}) \\ge 0.$$$

Lean4

theorem isPositive_iff_complex (T : E' →ₗ[ℂ] E') :
    IsPositive T ↔ ∀ x, (re ⟪T x, x⟫_ℂ : ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ := by
  simp_rw [IsPositive, forall_and, isSymmetric_iff_inner_map_self_real, conj_eq_iff_re, re_to_complex,
    Complex.coe_algebraMap]

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