Traces in inner product spaces

This file contains various results about traces of linear operators in inner product spaces.

theorem LinearMap.trace_eq_sum_inner {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) (b : OrthonormalBasis ι 𝕜 E) : (trace 𝕜 E) T = ∑ i : ι, inner 𝕜 (b i) (T (b i))

theorem LinearMap.IsSymmetric.trace_eq_sum_eigenvalues {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : (trace 𝕜 E) T = ↑(∑ i : Fin n, hT.eigenvalues hn i)

theorem LinearMap.IsSymmetric.re_trace_eq_sum_eigenvalues {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : RCLike.re ((trace 𝕜 E) T) = ∑ i : Fin n, hT.eigenvalues hn i

theorem InnerProductSpace.trace_rankOne {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (x y : E) : (LinearMap.trace 𝕜 E) ↑(((rankOne 𝕜) x) y) = inner 𝕜 y x