Eigenvalues/eigenvectors for Matrix.unitaryGroup

Stream: mathlib4

[Aaron Hill]

Currently, we only have eigenvalues/eigenvalues defined when a Matrix is hermitian (Matrix.IsHermitian.eigenvalues). I'm interested in extending this to support (at least) Matrix.unitaryGroup. What would be the best way to go about this?

• Add similar definitions/theorems to the Matrix.unitaryGroup submonoid (e.g. Matrix.unitaryGroup.eigenvalues, Matrix.unitaryGroup.spectral_theorem, etc)
• Add a new Matrix.IsUnitary prop (similar to IsHermitian), and add the API for plain Matrix types with a Matrix.IsUnitary hypothesis, rather than adding them to the Matrix.unitaryGroup submonoid
• Introduce a new IsNormal prop for matrices that commute with their conjugate transpose (A*A = AA*), define eigenvectors and (complex) eigenvalues, and prove the spectral theorem for normal matrices, rather than separately for unitary and hermitian matrices.

Since at least some of the proofs for Matrix.IsHermitian go through LinearMap.IsSymmetric, I assume that we'd also need to add LinearMap equivalents of some defintions above.

[Jireh Loreaux]

Here's an important question: for what purpose do you want the eigenvalues and eigenvectors of a unitary matrix? It's possible you can get away without them.

[Aaron Hill]

I'm working on formalizing a proof of Gromov's theorem of groups of polynomial growth (https://www.diva-portal.org/smash/get/diva2:1851013/FULLTEXT01.pdf). As part of this, I need: for a unitary matrix $g \in U(n)$ not equal to a multiple of the identity, the centralizer $Z(g)$ is isomorphic to a product of unitary subgroups with dimensions strictly smaller than $n$

[Aaron Hill]

and for that, I need to diagonalize g

[Jireh Loreaux]

You could probably just use the continuous functional calculus.

[Jireh Loreaux]

What you really want are the projections corresponding to each element of the spectrum, which is easier to get through the functional calculus anyway.

[Jireh Loreaux]

There's some code about commuting with cfc f a in the LeanOA repo. If you bug me about it in a day or two I can upstream it to Mathlib.

[Yaël Dillies]

Aaron Hill said:

I'm working on formalizing a proof of Gromov's theorem of groups of polynomial growth (https://www.diva-portal.org/smash/get/diva2:1851013/FULLTEXT01.pdf). As part of this, I need: for a unitary matrix $g \in U(n)$ not equal to a multiple of the identity, the centralizer $Z(g)$ is isomorphic to a product of unitary subgroups with dimensions strictly smaller than $n$

Any chance I could interest you in working with me on the Breuillard-Green-Tao theorem (which has Gromov as corollary) instead?

[Kevin Buzzard]

What's wrong with just looking at the roots of the char poly?

[Jireh Loreaux]

That doesn't really give you nice access to the projections.

[Frédéric Dupuis]

Jireh Loreaux said:

There's some code about commuting with cfc f a in the LeanOA repo. If you bug me about it in a day or two I can upstream it to Mathlib.

If @Aaron Hill doesn't bug you, then I will :-)

[Aaron Hill]

Jireh Loreaux said:

There's some code about commuting with cfc f a in the LeanOA repo. If you bug me about it in a day or two I can upstream it to Mathlib.

I'd definitely be interested in that - thanks!

[Aaron Hill]

Yaël Dillies said:

Aaron Hill said:

I'm working on formalizing a proof of Gromov's theorem of groups of polynomial growth (https://www.diva-portal.org/smash/get/diva2:1851013/FULLTEXT01.pdf). As part of this, I need: for a unitary matrix $g \in U(n)$ not equal to a multiple of the identity, the centralizer $Z(g)$ is isomorphic to a product of unitary subgroups with dimensions strictly smaller than $n$

Any chance I could interest you in working with me on the Breuillard-Green-Tao theorem (which has Gromov as corollary) instead?

I'm probably going to keep working on that proof, but I'd also be happy to work with you on Breuillard-Green-Tao

[Aaron Hill]

Aaron Hill said:

Currently, we only have eigenvalues/eigenvalues defined when a Matrix is hermitian (Matrix.IsHermitian.eigenvalues). I'm interested in extending this to support (at least) Matrix.unitaryGroup. What would be the best way to go about this?

• Add similar definitions/theorems to the Matrix.unitaryGroup submonoid (e.g. Matrix.unitaryGroup.eigenvalues, Matrix.unitaryGroup.spectral_theorem, etc)
• Add a new Matrix.IsUnitary prop (similar to IsHermitian), and add the API for plain Matrix types with a Matrix.IsUnitary hypothesis, rather than adding them to the Matrix.unitaryGroup submonoid
• Introduce a new IsNormal prop for matrices that commute with their conjugate transpose (A*A = AA*), define eigenvectors and (complex) eigenvalues, and prove the spectral theorem for normal matrices, rather than separately for unitary and hermitian matrices.

Since at least some of the proofs for Matrix.IsHermitian go through LinearMap.IsSymmetric, I assume that we'd also need to add LinearMap equivalents of some defintions above.

It turns out that IsStarNormal already exists, but there's no associated eigenvalue/eigenvector definitions for matrices

[Jireh Loreaux]

@Aaron Hill if you want to know why we don't have this, it's essentially for the reason I laid out here:
#maths > spectral theorem for normal endomorphisms and related pain @ 💬

The issue is that we don't currently have a nice way to refer to adjoints that works simultaneously for ContinuousLinearMap and for LinearMap. Thus you have a bunch of duplication.

[Jireh Loreaux]

I'm sure @Monica Omar cares about this problem too.

[Jireh Loreaux]

Here's some code I had from a while ago which adopts the "let there be duplication" approach to this problem. You can get the analogous statements for linear maps in finite dimensions using docs#LinearMap.toContinuousLinearMap

eigenvalues and eigenvectors of normal operators

import Mathlib

namespace IsStarNormal

section AddOfComm

variable {R : Type*} [Semiring R] [StarRing R] {x y : R} [IsStarNormal x] [IsStarNormal y]

lemma add_of_commute (h : Commute (star x) y) : IsStarNormal (x + y) where
  star_comm_self := by
    show _ = _
    have h' := commute_star_comm.mp h
    simp [add_mul, mul_add, star_comm_self', h.eq, h'.eq]
    abel

end AddOfComm


section Semiring

variable {R A : Type*} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A]
variable [StarModule R A] (x : A) [IsStarNormal x] (r : R)

instance _root_.algebraMap_isStarNormal : IsStarNormal (algebraMap R A r) where
  star_comm_self := Algebra.commute_algebraMap_right _ _

instance add_algebraMap : IsStarNormal (x + algebraMap R A r) := by
  exact add_of_commute (Algebra.commutes _ _).symm

instance algebraMap_add : IsStarNormal (algebraMap R A r + x) :=
  add_comm _ x ▸ add_algebraMap x r

end Semiring

section Ring

variable {R A : Type*} [CommRing R] [StarRing R] [Ring A] [StarRing A] [Algebra R A]
variable [StarModule R A] (x : A) [IsStarNormal x] (r : R)

instance sub_algebraMap : IsStarNormal (x - algebraMap R A r) := by
  rw [sub_eq_add_neg, ← map_neg]
  exact add_algebraMap _ _

instance algebraMap_sub : IsStarNormal (algebraMap R A r - x) := by
  rw [← neg_sub]
  infer_instance

end Ring

end IsStarNormal

namespace ContinuousLinearMap

variable {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
variable [CompleteSpace E] (f : E →L[𝕜] E) [IsStarNormal f]

lemma adjoint_apply_eq_zero_iff (x : E) : adjoint f x = 0 ↔ f x = 0 := by
  rw [← norm_eq_zero , norm_eq_sqrt_re_inner (𝕜 := 𝕜), adjoint_inner_left, ← mul_apply,
    ← star_eq_adjoint, ← star_comm_self, star_eq_adjoint, mul_apply, adjoint_inner_right,
    ← norm_eq_sqrt_re_inner, norm_eq_zero]

lemma ker_adjoint_eq_ker : LinearMap.ker (adjoint f) = LinearMap.ker f :=
  Submodule.ext <| adjoint_apply_eq_zero_iff f

open Module.End
lemma mem_eigenspace_adjoint_of_isStarNormal (μ : 𝕜) (x : E) :
    x ∈ Module.End.eigenspace (adjoint f) (star μ) ↔ x ∈ Module.End.eigenspace f μ := by
  simp only [mem_eigenspace_iff]
  convert adjoint_apply_eq_zero_iff (f := f - algebraMap 𝕜 (E →L[𝕜] E) μ) x using 1
  all_goals simp [sub_eq_zero, Algebra.algebraMap_eq_smul_one, ← star_eq_adjoint]

lemma adjoint_apply_eq_star_smul_self_iff (μ : 𝕜) (x : E) :
    adjoint f x = star μ • x ↔ f x = μ • x := by
  simpa [mem_eigenspace_iff] using mem_eigenspace_adjoint_of_isStarNormal f μ x

lemma adjoint_hasEigenvector_of_isStarNormal (μ : 𝕜) (x : E) :
    HasEigenvector (adjoint f) (star μ) x ↔ HasEigenvector f μ x :=
  and_congr_left' <| mem_eigenspace_adjoint_of_isStarNormal f μ x

-- MOVE ME to `LinearAlgebra.Eigenspace.Basic`
theorem _root_.Module.End.hasEigenvalue_iff_exists_hasEigenvector {R M : Type*} [CommRing R]
    [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} :
    HasEigenvalue f μ ↔ ∃ v, HasEigenvector f μ v :=
  ⟨HasEigenvalue.exists_hasEigenvector, by rintro ⟨v, hv⟩; exact hasEigenvalue_of_hasEigenvector hv⟩

lemma adjoint_hasEigenvalue_of_isStarNormal (μ : 𝕜) :
    HasEigenvalue (M := E) (adjoint f) (star μ) ↔ HasEigenvalue (M := E) f μ := by
  simp only [hasEigenvalue_iff_exists_hasEigenvector]
  peel 1
  exact adjoint_hasEigenvector_of_isStarNormal f μ _

lemma invariant_orthogonalComplement_eigenspace (μ : 𝕜) (v : E)
    (hv : v ∈ (Module.End.eigenspace f μ)ᗮ) : f v ∈ (Module.End.eigenspace f μ)ᗮ := by
  intro w hw
  have hw' := mem_eigenspace_adjoint_of_isStarNormal f μ w |>.mpr hw
  rw [mem_eigenspace_iff, coe_coe] at hw'
  rw [← adjoint_inner_left, hw', inner_smul_left, hv w hw, mul_zero]

/-- The eigenspaces of a normal operator are mutually orthogonal. -/
theorem orthogonalFamily_eigenspaces :
    OrthogonalFamily 𝕜 (eigenspace (f : E →ₗ[𝕜] E) ·)
      fun μ ↦ (eigenspace (f : E →ₗ[𝕜] E) μ).subtypeₗᵢ := by
  rintro μ ν hμν ⟨v, hv⟩ ⟨w, hw⟩
  by_cases hv' : v = 0
  · simp [hv']
  rw [← mem_eigenspace_adjoint_of_isStarNormal f ν w] at hw
  rw [mem_eigenspace_iff, coe_coe] at hv hw
  refine Or.resolve_left ?_ hμν.symm
  simp only [Submodule.coe_subtypeₗᵢ, Submodule.coe_subtype]
  simpa only [Submodule.coe_subtypeₗᵢ, Submodule.coe_subtype, ← RCLike.star_def, hw,
    inner_smul_right, hv, inner_smul_left, mul_eq_mul_right_iff, star_inj]
    using adjoint_inner_right f v w

theorem orthogonalFamily_eigenspaces' :
    OrthogonalFamily 𝕜 (fun μ : Eigenvalues (f : E →ₗ[𝕜] E) ↦ eigenspace (f : E →ₗ[𝕜] E) μ)
      fun μ ↦ (eigenspace (f : E →ₗ[𝕜] E) μ).subtypeₗᵢ :=
  f.orthogonalFamily_eigenspaces.comp Subtype.coe_injective

/-- The mutual orthogonal complement of the eigenspaces of a normal operator on an inner
product space is an invariant subspace of the operator. -/
theorem orthogonalComplement_iSup_eigenspaces_invariant ⦃v : E⦄
    (hv : v ∈ (⨆ μ, eigenspace (f : E →ₗ[𝕜] E) μ)ᗮ) :
    f v ∈ (⨆ μ, eigenspace (f : E →ₗ[𝕜] E) μ)ᗮ := by
  rw [← Submodule.iInf_orthogonal] at hv ⊢
  exact f.iInf_invariant f.invariant_orthogonalComplement_eigenspace v hv

/-- The mutual orthogonal complement of the eigenspaces of a normal operator on an inner
product space has no eigenvalues. -/
theorem orthogonalComplement_iSup_eigenspaces (μ : 𝕜) :
    eigenspace (f.restrict f.orthogonalComplement_iSup_eigenspaces_invariant) μ = ⊥ := by
  set p : Submodule 𝕜 E := (⨆ μ, eigenspace (f : E →ₗ[𝕜] E) μ)ᗮ
  refine' eigenspace_restrict_eq_bot f.orthogonalComplement_iSup_eigenspaces_invariant _
  have H₂ : eigenspace (f : E →ₗ[𝕜] E) μ ⟂ p := (Submodule.isOrtho_orthogonal_right _).mono_left
    (le_iSup _ _)
  exact H₂.disjoint

end ContinuousLinearMap

[Monica Omar]

some of this stuff should probably go in Mathlib

[Jireh Loreaux]

Feel free to PR if that's what you think should happen, but I won't be able to merge it for obvious reasons. I've been hoping to come up with a solution to the problem in the other thread, but still haven't come up with anything satisfying, despite thinking about it again for an hour or two yesterday.

[Aaron Hill]

Jireh Loreaux said:

There's some code about commuting with cfc f a in the LeanOA repo. If you bug me about it in a day or two I can upstream it to Mathlib.

Did that end up getting upstreamed?

[Jireh Loreaux]

Yes. docs#Commute.cfc

[Aaron Hill]

Do you have any examples of code that projects to a lower-dimensional matrix using the CFC?

[Jireh Loreaux]

I'm not sure what you mean, please expand on what you're asking for.

[Aaron Hill]

I was referring to your earlier comment:

What you really want are the projections corresponding to
each element of the spectrum, which is easier to get through the
functional calculus anyway.

and I was assuming that these projections would in some way correspond to matrices with lower dimension than the original one

[Jireh Loreaux]

Ah, no, i just meant a projection in the sense that P = star P = P ^ 2