diagonal — Mathlib

English

A diagonal matrix diagonal(d) is PosDef iff each d_i > 0.

Русский

Диагональная матрица diag(d) PosDef ⇔ ∀ i, d_i > 0.

LaTeX

$$PosDef( diagonal(d) ) ↔ ∀ i, d_i > 0$$

Lean4

protected theorem diagonal [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] {d : n → R} (h : ∀ i, 0 < d i) :
    PosDef (diagonal d) :=
  ⟨isHermitian_diagonal_of_self_adjoint _ <| funext fun i => IsSelfAdjoint.of_nonneg (h i).le, fun x hx =>
    by
    refine Fintype.sum_pos ?_
    simp_rw [mulVec_diagonal, ← mul_assoc, Pi.lt_def]
    obtain ⟨i, hi⟩ := Function.ne_iff.mp hx
    exact ⟨fun i => conjugate_nonneg (h i).le _, i, conjugate_pos (h _) (isRegular_of_ne_zero hi)⟩⟩

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