smul — Mathlib

English

If x is PSD and α ≥ 0 is a scalar, then α x is PSD.

Русский

Если x ПСД и α ≥ 0 — скаляр, то α x ПСД.

LaTeX

$$$\alpha \ge 0 \Rightarrow (\alpha x) \text{ PosSemidef}$ for $x$ PSD$$

Lean4

protected theorem smul {α : Type*} [CommSemiring α] [PartialOrder α] [StarRing α] [StarOrderedRing α] [Algebra α R]
    [StarModule α R] [PosSMulMono α R] {x : Matrix n n R} (hx : x.PosSemidef) {a : α} (ha : 0 ≤ a) :
    (a • x).PosSemidef :=
  by
  refine ⟨IsSelfAdjoint.smul (IsSelfAdjoint.of_nonneg ha) hx.1, fun y => ?_⟩
  simp only [smul_mulVec, dotProduct_smul]
  exact smul_nonneg ha (hx.2 _)

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