isPositive_iff_isSymmetric — Mathlib

English

If T is positive, then Re⟪Tx, x⟫ ≥ 0 for all x.

Русский

Если T положителен, то Re⟪Tx, x⟫ ≥ 0 для всех x.

LaTeX

$$$$\forall x, \; \operatorname{Re}\langle Tx, x \rangle \ge 0.$$$$

Lean4

/-- An idempotent linear map is positive iff it is symmetric. -/
theorem isPositive_iff_isSymmetric {T : E →ₗ[𝕜] E} (hT : IsIdempotentElem T) : T.IsPositive ↔ T.IsSymmetric :=
  by
  refine ⟨fun h => h.isSymmetric, fun h => ⟨h, fun x => ?_⟩⟩
  rw [← hT.eq, Module.End.mul_apply, h]
  exact inner_self_nonneg

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