English
For a positive endomorphism T, ⟪Tx, x⟫ = ⟪x, Tx⟫ for all x.
Русский
Для положительного эндоморфизма T выполняется для всех x: ⟪Tx, x⟫ = ⟪x, Tx⟫.
LaTeX
$$$$\forall x, \; \langle Tx, x \rangle = \langle x, Tx \rangle.$$$$
Lean4
/-- The (Loewner) partial order on linear maps on a Hilbert space determined by `f ≤ g`
if and only if `g - f` is a positive linear map (in the sense of `LinearMap.IsPositive`). -/
instance instLoewnerPartialOrder : PartialOrder (E →ₗ[𝕜] E)
where
le f g := (g - f).IsPositive
le_refl _ := by simp
le_trans _ _ _ h₁ h₂ := by simpa using h₁.add h₂
le_antisymm f₁ f₂ h₁
h₂ := by
rw [← sub_eq_zero, ← h₂.isSymmetric.inner_map_self_eq_zero]
intro x
have hba2 := h₁.2 x
rw [← neg_le_neg_iff, ← map_neg, ← inner_neg_left, ← neg_apply, neg_sub, neg_zero] at hba2
rw [← h₂.isSymmetric.coe_re_inner_apply_self, RCLike.ofReal_eq_zero]
exact le_antisymm hba2 (h₂.2 _)
