Inner product of Hermitian Matrices

For general matrices there are multiple reasonable notions of "inner product" (Hilbert–Schmidt inner product, Frobenius inner product), and so Mathlib avoids giving a canonical InnerProductSpace instance. But for the particular case of Hermitian matrices, these all coincide, so we can put a canonical InnerProductSpace instance.

This does however induce a Norm on HermitianMat as well, the Frobenius norm, and this is less obviously a uniquely correct choice. It is something that one essentially has to live with, with the way that Mathlib currently structures the instances. (Thankfully, all norms induce the same topology and bornology on finite-dimensional matrices.)

Some care to be taken so that the topology induced by the InnerProductSpace is defeq with the Subtype topology that HermitianMat inherits from the topology on Matrix. This can be done via InnerProductSpace.ofCoreOfTopology.

def HermitianMat.inner {R : Type u_1} {n : Type u_2} {α : Type u_3} [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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem HermitianMat.inner_left_neg {R : Type u_1} {n : Type u_2} {α : Type u_3} [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_1} {n : Type u_2} {α : Type u_3} [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_1} {n : Type u_2} {α : Type u_3} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B C : HermitianMat n α) : A.inner (B - C) = A.inner B - A.inner C

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

@[simp]

theorem HermitianMat.smul_inner {R : Type u_1} {n : Type u_2} {α : Type u_3} [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_1} {n : Type u_2} {α : Type u_3} [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

def HermitianMat.inner_BilinForm {R : Type u_1} {n : Type u_2} {α : Type u_3} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] [StarModule R α] : LinearMap.BilinForm R (HermitianMat n α)

The Hermitian inner product as bilinear form.

Equations

• HermitianMat.inner_BilinForm = { toFun := fun (A : HermitianMat n α) => { toFun := A.inner, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem HermitianMat.inner_one {R : Type u_1} {n : Type u_2} {α : Type u_3} [Star R] [TrivialStar R] [Fintype n] [CommSemiring 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_1} {n : Type u_2} {α : Type u_3} [Star R] [TrivialStar R] [Fintype n] [CommSemiring 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_1} {n : Type u_2} {α : Type u_3} [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_1} {n : Type u_2} {α : Type u_3} [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 {n : Type u_2} {α : Type u_3} [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_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] (A B : HermitianMat n 𝕜) : A.inner B = RCLike.re (↑A * ↑B).trace

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

theorem HermitianMat.inner_self_nonneg {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] (A : HermitianMat n 𝕜) : 0 ≤ A.inner A

theorem HermitianMat.inner_mul_nonneg {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A B : HermitianMat n 𝕜} (h : 0 ≤ ↑A * ↑B) : 0 ≤ A.inner B

theorem HermitianMat.inner_ge_zero {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A B : HermitianMat n 𝕜} (hA : 0 ≤ A) (hB : 0 ≤ B) : 0 ≤ A.inner B

The inner product for PSD matrices is nonnegative.

theorem HermitianMat.inner_mono {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A B C : HermitianMat n 𝕜} (hA : 0 ≤ A) : B ≤ C → A.inner B ≤ A.inner C

theorem HermitianMat.inner_mono' {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A B C : HermitianMat n 𝕜} (hA : 0 ≤ A) : B ≤ C → B.inner A ≤ C.inner A

theorem HermitianMat.inner_le_mul_trace {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A B : HermitianMat 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.inner_zero_iff {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A B : HermitianMat n 𝕜} [DecidableEq n] (hA₁ : 0 ≤ A) (hB₁ : 0 ≤ B) : A.inner B = 0 ↔ A.support ≤ B.ker

The inner product of two PSD matrices is zero iff they have disjoint support, i.e., each lives entirely in the other's kernel.

@[simp]

theorem HermitianMat.reindex_inner {𝕜 : Type u_5} [RCLike 𝕜] {d : Type u_6} {d₂ : Type u_7} (A : HermitianMat d 𝕜) [Fintype d₂] [Fintype d] (e : d ≃ d₂) (B : HermitianMat d₂ 𝕜) : (A.reindex e).inner B = A.inner (B.reindex e.symm)

Theorems about HermitianMats that have to do with the topological structure. Pretty much everything here will assume these are matrices over ℂ, but changes to upgrade this to other types are welcome.

instance HermitianMat.instContinuousSMulReal {d : Type u_4} {𝕜 : Type u_5} [RCLike 𝕜] : ContinuousSMul ℝ (HermitianMat d 𝕜)

theorem HermitianMat.inner_bilinForm_Continuous {d : Type u_4} [Fintype d] {𝕜 : Type u_5} [RCLike 𝕜] (A : HermitianMat d 𝕜) : Continuous ⇑(inner_BilinForm A)

theorem HermitianMat.inner_continuous {d : Type u_4} [Fintype d] {𝕜 : Type u_5} [RCLike 𝕜] : Continuous (Function.uncurry inner)

noncomputable def HermitianMat.InnerProductCore {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] : InnerProductSpace.Core ℝ (HermitianMat d 𝕜)

We define the Hermitian inner product as our "canonical" inner product, which does induce a norm. This disagrees slightly with Mathlib convention on the Matrix type, which avoids asserting one norm as there are several reasonable ones; for Hermitian matrices, though, this seem to be the right choice.

Equations

• HermitianMat.InnerProductCore = { inner := fun (A B : HermitianMat d 𝕜) => A.inner B, conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯, definite := ⋯ }

noncomputable instance HermitianMat.instNormedGroup {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] : NormedAddCommGroup (HermitianMat d 𝕜)

The HermitianMat type inherits the Frobenius necessarily, since it's going to need the Hermitian inner product, and in Mathlib an InnerProductSpace always carries the corresponding norm.

Equations

• HermitianMat.instNormedGroup = AddSubgroupClass.normedAddCommGroup (selfAdjoint (Matrix d d 𝕜))

theorem HermitianMat.norm_eq_frobenius {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] (A : HermitianMat d 𝕜) : ‖A‖ = (∑ i : d, ∑ j : d, ‖A i j‖ ^ 2) ^ (1 / 2)

@[simp]

theorem HermitianMat.toMat_apply {d : Type u_4} {𝕜 : Type u_6} [RCLike 𝕜] {A : HermitianMat d 𝕜} {i j : d} : ↑A i j = A i j

theorem HermitianMat.norm_eq_sqrt_inner_self {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] (A : HermitianMat d 𝕜) : ‖A‖ = √(A.inner A)

noncomputable instance HermitianMat.instNormedSpace {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] : NormedSpace ℝ (HermitianMat d 𝕜)

Equations

• HermitianMat.instNormedSpace = { toModule := selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule, norm_smul_le := ⋯ }

noncomputable instance HermitianMat.instInnerProductSpace {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] : InnerProductSpace ℝ (HermitianMat d 𝕜)

Equations

• One or more equations did not get rendered due to their size.

theorem HermitianMat.inner_eq {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] (A B : HermitianMat d 𝕜) : Inner.inner ℝ A B = A.inner B

instance HermitianMat.instCompleteSpace {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] : CompleteSpace (HermitianMat d 𝕜)

noncomputable instance HermitianMat.instNormedAddCommGroupReal {d : Type u_4} [Fintype d] : NormedAddCommGroup (HermitianMat d ℝ)

Equations

• HermitianMat.instNormedAddCommGroupReal = inferInstance

noncomputable instance HermitianMat.instNormedAddCommGroupComplex {d : Type u_4} [Fintype d] : NormedAddCommGroup (HermitianMat d ℂ)

Equations

• HermitianMat.instNormedAddCommGroupComplex = inferInstance

def RCLike.instOrderClosed {𝕜 : Type u_6} [RCLike 𝕜] : OrderClosedTopology 𝕜

Equations

• ⋯ = ⋯

theorem HermitianMat.inner_ge_zero' {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] (A B : HermitianMat d 𝕜) (hA : 0 ≤ A) (hB : 0 ≤ B) : 0 ≤ Inner.inner ℝ A B

The inner product for PSD matrices is nonnegative.

theorem HermitianMat.dist_le_of_mem_Icc {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] {A B : HermitianMat d 𝕜} (x : HermitianMat d 𝕜) (hA : A ≤ x) (hB : x ≤ B) : ‖x - A‖ ≤ ‖B - A‖

theorem HermitianMat.Matrix.IsHermitian_isClosed {n : Type u_2} {𝕜 : Type u_6} [RCLike 𝕜] : IsClosed {A : Matrix n n 𝕜 | A.IsHermitian}

theorem HermitianMat.Matrix.PosSemiDef_isClosed {n : Type u_2} [Fintype n] {𝕜 : Type u_6} [RCLike 𝕜] : IsClosed {A : Matrix n n 𝕜 | A.PosSemidef}

theorem HermitianMat.isClosed_nonneg {n : Type u_2} [Fintype n] {𝕜 : Type u_6} [RCLike 𝕜] : IsClosed {A : HermitianMat n 𝕜 | 0 ≤ A}

instance HermitianMat.instOrderClosedTopology {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] : OrderClosedTopology (HermitianMat d 𝕜)

instance HermitianMat.instCompactIccSpace {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] : CompactIccSpace (HermitianMat d 𝕜)

Equivalently: the matrices X such that X - A is PSD and B - X is PSD, form a compact set.

theorem HermitianMat.unitInterval_IsCompact {d : Type u_4} [Fintype d] {𝕜 : Type u_6} [RCLike 𝕜] [DecidableEq d] : IsCompact {m : HermitianMat d 𝕜 | 0 ≤ m ∧ m ≤ 1}

The PSD matrices that are ≤ 1 are a compact set. More generally, this is true of any closed interval, but stating that is a bit different because of how numerals are treated. The 0 and 1 here are already directly matrices, putting in an (a : ℝ) • 1 ≤ m ∧ m ≤ (b : ℝ) • 1 involves casts. But that theorem should follow easily from this. More generally A ≤ m ∧ m ≤ B is compact.