instance HermitianMat.instPartialOrder {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] : PartialOrder (HermitianMat n α)

The MatrixOrder instance for Matrix (the Loewner order) we keep open for HermitianMat, always.

Equations

• HermitianMat.instPartialOrder = inferInstance

theorem HermitianMat.le_iff {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] {A B : HermitianMat n α} : A ≤ B ↔ (↑(B - A)).PosSemidef

theorem HermitianMat.zero_le_iff {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] {A : HermitianMat n α} : 0 ≤ A ↔ (↑A).PosSemidef

theorem HermitianMat.le_iff_mulVec_le {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] {A B : HermitianMat n α} : A ≤ B ↔ ∀ (x : n → α), star x ⬝ᵥ (↑A).mulVec x ≤ star x ⬝ᵥ (↑B).mulVec x

instance HermitianMat.instZeroLEOneClassComplex {n : Type u_2} [Fintype n] [DecidableEq n] : ZeroLEOneClass (HermitianMat n ℂ)

theorem HermitianMat.lt_iff_posdef {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] {A B : HermitianMat n α} : A < B ↔ (↑(B - A)).PosSemidef ∧ A ≠ B

instance HermitianMat.instIsStrictOrderedModuleReal {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] : IsStrictOrderedModule ℝ (HermitianMat n α)

instance HermitianMat.instPosSMulMonoReal {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] : PosSMulMono ℝ (HermitianMat n α)

instance HermitianMat.instSMulPosMonoReal {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] : SMulPosMono ℝ (HermitianMat n α)

theorem HermitianMat.le_trace_smul_one {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] {A : HermitianMat n α} [DecidableEq n] (hA : 0 ≤ A) : A ≤ A.trace • 1

theorem HermitianMat.conj_le {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] {A : HermitianMat n α} {m : Type u_3} (hA : 0 ≤ A) [Fintype m] (M : Matrix m n α) : 0 ≤ (conj M) A

theorem HermitianMat.convex_cone {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] {A B : HermitianMat n α} (hA : 0 ≤ A) (hB : 0 ≤ B) {c₁ c₂ : ℝ} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) : 0 ≤ c₁ • A + c₂ • B

theorem HermitianMat.sq_nonneg {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] {A : HermitianMat n α} [DecidableEq n] : 0 ≤ A ^ 2

theorem HermitianMat.ker_antitone {α : Type u_1} [RCLike α] {n : Type u_2} [Fintype n] {A B : HermitianMat n α} [DecidableEq n] (hA : 0 ≤ A) : A ≤ B → B.ker ≤ A.ker