class IsMaximalSelfAdjoint (R : outParam (Type u_1)) (α : Type u_2) [Star α] [Star R] [CommSemiring R] [Semiring α] [TrivialStar R] [Algebra R α] : Type (max u_1 u_2)

• selfadjMap : α →+ R
• selfadj_smul (r : R) (a : α) : selfadjMap (r • a) = r * selfadjMap a
• selfadj_algebra {a : α} : IsSelfAdjoint a → (algebraMap R α) (selfadjMap a) = a

instance instTrivialStar_IsMaximalSelfAdjoint {R : Type u_1} [Star R] [TrivialStar R] [CommSemiring R] : IsMaximalSelfAdjoint R R

Every TrivialStar CommSemiring is its own maximal self adjoints.

Equations

• instTrivialStar_IsMaximalSelfAdjoint = { selfadjMap := AddMonoidHom.id R, selfadj_smul := ⋯, selfadj_algebra := ⋯ }

instance instRCLike_IsMaximalSelfAdjoint {α : Type u_1} [RCLike α] : IsMaximalSelfAdjoint ℝ α

ℝ is the maximal self adjoint elements over RCLike

Equations

• instRCLike_IsMaximalSelfAdjoint = { selfadjMap := RCLike.re, selfadj_smul := ⋯, selfadj_algebra := ⋯ }

@[reducible, inline]

abbrev HermitianMat (n : Type u_1) (α : Type u_2) [AddGroup α] [StarAddMonoid α] : Type (max u_1 u_2)

The type of Hermitian matrices, as a Subtype. Equivalent to a Matrix n n α bundled with the fact that Matrix.IsHermitian.

Equations

• HermitianMat n α = ↥(selfAdjoint (Matrix n n α))

theorem HermitianMat.eq_IsHermitian {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] : HermitianMat n α = { m : Matrix n n α // m.IsHermitian }

@[reducible]

def HermitianMat.toMat {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] : HermitianMat n α → Matrix n n α

Equations

• HermitianMat.toMat = Subtype.val

instance HermitianMat.instCoeMatrix {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] : Coe (HermitianMat n α) (Matrix n n α)

Equations

• HermitianMat.instCoeMatrix = { coe := HermitianMat.toMat }

@[simp]

theorem HermitianMat.val_eq_coe {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] (A : HermitianMat n α) : ↑A = ↑A

@[simp]

theorem HermitianMat.mk_toMat {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] (x : Matrix n n α) (h : x ∈ selfAdjoint (Matrix n n α)) : ↑⟨x, h⟩ = x

theorem HermitianMat.H {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] (A : HermitianMat n α) : (↑A).IsHermitian

Alias for HermitianMat.property or HermitianMat.2, this gets the fact that the value is actually IsHermitian.

theorem HermitianMat.ext {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] {A B : HermitianMat n α} : ↑A = ↑B → A = B

instance HermitianMat.instFun {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] : FunLike (HermitianMat n α) n (n → α)

Equations

• HermitianMat.instFun = { coe := fun (M : HermitianMat n α) => ↑M, coe_injective' := ⋯ }

instance HermitianMat.instStar {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] : Star (HermitianMat n α)

Equations

• HermitianMat.instStar = { star := fun (x : HermitianMat n α) => x }

instance HermitianMat.instTrivialStar {α : Type u_1} {n : Type u_2} [AddGroup α] [StarAddMonoid α] : TrivialStar (HermitianMat n α)

noncomputable instance HermitianMat.instInv {α : Type u_1} {n : Type u_2} [CommRing α] [StarRing α] [DecidableEq n] [Fintype n] : Inv (HermitianMat n α)

Equations

• HermitianMat.instInv = { inv := fun (x : HermitianMat n α) => ⟨(↑x)⁻¹, ⋯⟩ }

noncomputable instance HermitianMat.instZPow {α : Type u_1} {n : Type u_2} [CommRing α] [StarRing α] [DecidableEq n] [Fintype n] : Pow (HermitianMat n α) ℤ

Equations

• HermitianMat.instZPow = { pow := fun (x : HermitianMat n α) (z : ℤ) => ⟨↑x ^ z, ⋯⟩ }

instance HermitianMat.instStarModuleReal {α : Type u_3} [RCLike α] : StarModule ℝ α

def HermitianMat.conj {α : Type u_1} {n : Type u_2} [CommRing α] [StarRing α] [Fintype n] {m : Type u_3} (A : HermitianMat n α) (B : Matrix m n α) : HermitianMat m α

The Hermitian matrix given by conjugating by a (possibly rectangular) Matrix. If we required B to be square, this would apply to any Semigroup+StarMul (as proved by IsSelfAdjoint.conjugate). But this lets us conjugate to other sizes too, as is done in e.g. Kraus operators. That is, it's a heterogeneous conjguation.

Equations

• A.conj B = ⟨B * ↑A * B.conjTranspose, ⋯⟩

def HermitianMat.trace {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [AddGroup α] [StarAddMonoid α] [CommSemiring R] [Semiring α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A : HermitianMat n α) : R

The trace of the matrix. This requires a IsMaximalSelfAdjoint R α instance, and then maps from HermitianMat n α to R. This means that the trace of (say) a HermitianMat n ℤ gives values in ℤ, but that the trace of a HermitianMat n ℂ gives values in ℝ. The fact that traces are "automatically" real reduces coercions down the line.

Equations

• A.trace = IsMaximalSelfAdjoint.selfadjMap (↑A).trace

theorem HermitianMat.trace_eq_trace {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [AddGroup α] [StarAddMonoid α] [CommSemiring R] [Semiring α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A : HermitianMat n α) : (algebraMap R α) A.trace = (↑A).trace

HermitianMat.trace reduces to Matrix.trace in the algebra.

@[simp]

theorem HermitianMat.trace_smul {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [AddGroup α] [StarAddMonoid α] [CommSemiring R] [Semiring α] [Algebra R α] [IsMaximalSelfAdjoint R α] [StarModule R α] (A : HermitianMat n α) (r : R) : (r • A).trace = r * A.trace

@[simp]

theorem HermitianMat.trace_zero {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommSemiring R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] : trace 0 = 0

@[simp]

theorem HermitianMat.trace_add {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommSemiring R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) : (A + B).trace = A.trace + B.trace

@[simp]

theorem HermitianMat.trace_neg {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A : HermitianMat n α) : (-A).trace = -A.trace

@[simp]

theorem HermitianMat.trace_sub {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) : (A - B).trace = A.trace - B.trace

@[simp]

theorem HermitianMat.trace_eq_trace_trivial {n : Type u_2} [Fintype n] (A : HermitianMat n ℝ) : A.trace = (↑A).trace

HermitianMat.trace reduces to Matrix.trace when the elements are a TrivialStar.

theorem HermitianMat.trace_eq_re_trace {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] (A : HermitianMat n 𝕜) : A.trace = RCLike.re (↑A).trace

@[simp]

theorem HermitianMat.trace_eq_trace_rc {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] (A : HermitianMat n 𝕜) : ↑A.trace = (↑A).trace

HermitianMat.trace reduces to Matrix.trace when the elements are RCLike.

def HermitianMat.inner {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [Ring α] [StarAddMonoid α] [CommSemiring R] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) : R

The Hermitian inner product, Tr[AB]. This is equal to Matrix.trace (A * B), but gives real values when the matrices are complex, using IsMaximalSelfAdjoint.

Equations

• A.inner B = IsMaximalSelfAdjoint.selfadjMap (↑A * ↑B).trace

@[simp]

theorem HermitianMat.inner_left_neg {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) : (-A).inner B = -A.inner B

@[simp]

theorem HermitianMat.inner_right_neg {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) : A.inner (-B) = -A.inner B

theorem HermitianMat.inner_left_sub {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) {C : HermitianMat n α} : A.inner (B - C) = A.inner B - A.inner C

theorem HermitianMat.inner_right_sub {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) {C : HermitianMat n α} : (A - B).inner C = A.inner C - B.inner C

@[simp]

theorem HermitianMat.inner_zero {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A : HermitianMat n α) : A.inner 0 = 0

@[simp]

theorem HermitianMat.zero_inner {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A : HermitianMat n α) : inner 0 A = 0

theorem HermitianMat.inner_left_distrib {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) {C : HermitianMat n α} : A.inner (B + C) = A.inner B + A.inner C

theorem HermitianMat.inner_right_distrib {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) {C : HermitianMat n α} : (A + B).inner C = A.inner C + B.inner C

@[simp]

theorem HermitianMat.smul_inner {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) [StarModule R α] (r : R) : (r • A).inner B = r * A.inner B

@[simp]

theorem HermitianMat.inner_smul {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) [StarModule R α] (r : R) : A.inner (r • B) = r * A.inner B

@[simp]

theorem HermitianMat.inner_one {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarRing α] [Algebra R α] [IsMaximalSelfAdjoint R α] [DecidableEq n] (A : HermitianMat n α) : A.inner 1 = A.trace

@[simp]

theorem HermitianMat.one_inner {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarRing α] [Algebra R α] [IsMaximalSelfAdjoint R α] [DecidableEq n] (A : HermitianMat n α) : inner 1 A = A.trace

theorem HermitianMat.inner_eq_trace_mul {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommSemiring R] [CommRing α] [StarRing α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) : (algebraMap R α) (A.inner B) = (↑A * ↑B).trace

The inner product for Hermtian matrices is equal to the trace of the product.

theorem HermitianMat.inner_comm {R : Type u_3} {α : Type u_1} {n : Type u_2} [Star R] [TrivialStar R] [Fintype n] [CommSemiring R] [CommRing α] [StarRing α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) : A.inner B = B.inner A

theorem HermitianMat.inner_eq_trace_trivial {α : Type u_1} {n : Type u_2} [Fintype n] [CommRing α] [StarRing α] [TrivialStar α] (A B : HermitianMat n α) : A.inner B = (↑A * ↑B).trace

HermitianMat.inner reduces to Matrix.trace (A * B) when the elements are a TrivialStar.

theorem HermitianMat.inner_eq_re_trace {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] (A B : HermitianMat n 𝕜) : A.inner B = RCLike.re (↑A * ↑B).trace

theorem HermitianMat.inner_eq_trace_rc {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] (A B : HermitianMat n 𝕜) : ↑(A.inner B) = (↑A * ↑B).trace

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

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

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

theorem HermitianMat.inner_ge_zero {α : Type u_1} {n : Type u_2} [Fintype n] [RCLike α] {A B : HermitianMat n α} [DecidableEq n] (hA : 0 ≤ A) (hB : 0 ≤ B) : 0 ≤ A.inner B

The inner product for PSD matrices is nonnegative.

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

theorem HermitianMat.inner_le_mul_trace {α : Type u_1} {n : Type u_2} [Fintype n] [RCLike α] {A B : HermitianMat n α} [DecidableEq n] (hA : 0 ≤ A) (hB : 0 ≤ B) : A.inner B ≤ A.trace * B.trace

The inner product for PSD matrices is at most the product of their traces.

theorem HermitianMat.convex_cone {α : Type u_1} {n : Type u_2} [Fintype n] [RCLike α] {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.conj_le {α : Type u_1} {n : Type u_2} [Fintype n] [RCLike α] {A : HermitianMat n α} {m : Type u_3} (hA : 0 ≤ A) [Fintype m] (M : Matrix m n α) : 0 ≤ A.conj M

def HermitianMat.rpow {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] (A : HermitianMat n 𝕜) (p : ℝ) : HermitianMat n 𝕜

Matrix power of a positive semidefinite matrix, as given by the elementwise real power of the diagonal in a diagonalized form.

Note that this has the usual Real.rpow caveats, such as 0 to the power -1 giving 0.

Equations

• A.rpow p = ⟨cfc (fun (x : ℝ) => x.rpow p) ↑A, ⋯⟩

noncomputable instance HermitianMat.instRPow {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] : Pow (HermitianMat n 𝕜) ℝ

Equations

• HermitianMat.instRPow = { pow := HermitianMat.rpow }

theorem HermitianMat.rpow_PosSemidef {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} (hA : (↑A).PosSemidef) (p : ℝ) : (↑(A ^ p)).PosSemidef

def HermitianMat.log {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] (A : HermitianMat n 𝕜) : HermitianMat n 𝕜

Matrix logarithm (base e) of a Hermitian matrix, as given by the elementwise real logarithm of the diagonal in a diagonalized form, using Real.log

Note that this means that the nullspace of the image includes all of the nullspace of the original matrix. This contrasts to the standard definition, which is only defined for positive definite matrices, and the nullspace of the image is exactly the (λ=1)-eigenspace of the original matrix. It coincides with the standard definition if A is positive definite.

Equations

• A.log = ⟨CFC.log ↑A, ⋯⟩