isPositive_iff_complex — Mathlib

English

For a complex Hilbert space, IsPositive T is equivalent to the real part criterion: the real part of ⟪T x, x⟫ equals ⟪T x, x⟫ and is nonnegative for all x.

Русский

Для комплексного пространства с скалярным произведением: IsPositive T эквивалентно условию по действительной части: действительная часть ⟪T x, x⟫ равна ⟪T x, x⟫ и неотрицательна для всех x.

LaTeX

$$$\text{IsPositive}(T) \iff \forall x, Re⟪T x, x⟫ = ⟪T x, x⟫ \wedge 0 \le Re⟪T x, x⟫$$$

Lean4

theorem isPositive_iff_complex (T : E' →L[ℂ] E') :
    IsPositive T ↔ ∀ x, (re ⟪T x, x⟫_ℂ : ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ := by
  simp [← isPositive_toLinearMap_iff, LinearMap.isPositive_iff_complex]

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