@[simp]

theorem LinearMap.unitary_star_apply_eq {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U : ↥(unitary (E →ₗ[𝕜] E))) (v : E) : (star ↑U) (↑U v) = v

@[simp]

theorem LinearMap.unitary_apply_star_eq {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U : ↥(unitary (E →ₗ[𝕜] E))) (v : E) : ↑U ((star ↑U) v) = v

noncomputable def LinearMap.conj_unitary_eigenspace_equiv {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (U : ↥(unitary (E →ₗ[𝕜] E))) (μ : 𝕜) : ↥(Module.End.eigenspace T μ) ≃ₗ[𝕜] ↥(Module.End.eigenspace (↑U * T * star ↑U) μ)

Conjugating a linear map by a unitary operator gives a map whose μ-eigenspace is isomorphic (same dimension) as those of the original linear map.

Equations

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

theorem LinearMap.IsSymmetric.conj_unitary_IsSymmetric {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (U : ↥(unitary (E →ₗ[𝕜] E))) (hT : T.IsSymmetric) : (↑U * T * star ↑U).IsSymmetric

A symmetric operator conjugated by a unitary is symmetric.

def LinearMap.IsSymmetric.conj_unitary_eigenvalue_equiv {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hn : Module.finrank 𝕜 E = n) (U : ↥(unitary (E →ₗ[𝕜] E))) (hT : T.IsSymmetric) : { σ : Equiv.Perm (Fin n) // ⋯.eigenvalues hn = hT.eigenvalues hn ∘ ⇑σ }

There is an equivalence between the eigenvalues of a finite dimensional symmetric operator, and the eigenvalues of that operator conjugated by a unitary.

Equations

• LinearMap.IsSymmetric.conj_unitary_eigenvalue_equiv hn U hT = sorry