isPositive_toContinuousLinearMap_iff

English

For a positive linear operator T, Re⟪x, Tx⟫ ≥ 0 for all x.

Русский

Положительный линейный оператор T удовлетворяет Re⟪x, Tx⟫ ≥ 0 для всех x.

LaTeX

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

Lean4

theorem _root_.LinearMap.isPositive_toContinuousLinearMap_iff [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) :
    have : CompleteSpace E := FiniteDimensional.complete 𝕜 _
    T.toContinuousLinearMap.IsPositive ↔ T.IsPositive :=
  by
  simp only [IsPositive, isSelfAdjoint_iff_isSymmetric, coe_toContinuousLinearMap, reApplyInnerSelf,
    coe_toContinuousLinearMap', LinearMap.IsPositive]

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