smul_of_nonneg — Mathlib

English

The Loewner partial order on linear maps on a Hilbert space is defined by f ≤ g iff g − f is positive.

Русский

Лоувнеров частичный порядок на линейных отображениях гильбертового пространства задаётся так: f ≤ g тогда и только если g − f положительно.

LaTeX

$$$$f \le g \;\Longleftrightarrow\; (g - f) \text{ is positive}.$$$$

Lean4

@[aesop safe apply]
theorem smul_of_nonneg {T : E →ₗ[𝕜] E} (hT : T.IsPositive) {c : 𝕜} (hc : 0 ≤ c) : (c • T).IsPositive :=
  by
  have hc' : starRingEnd 𝕜 c = c := by simp [conj_eq_iff_im, ← (le_iff_re_im.mp hc).right]
  refine ⟨hT.left.smul hc', fun x => ?_⟩
  rw [smul_apply, inner_smul_left, hc', mul_re, conj_eq_iff_im.mp hc', zero_mul, sub_zero]
  exact mul_nonneg ((re_nonneg_of_nonneg hc').mpr hc) (re_inner_nonneg_left hT x)

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