[Merged by Bors] - feat(analysis/inner_product_space/spectrum): diagonalization of self-adjoint endomorphisms (finite dimension)

[hrmacbeth]

Diagonalization of a self-adjoint endomorphism T of a finite-dimensional inner product space E over either ℝ or ℂ: construct a linear isometry T.diagonalization from E to the direct sum of T's eigenspaces, such that T conjugated by T.diagonalization is diagonal:

lemma diagonalization_apply_self_apply (v : E) (μ : eigenvalues T) :
  hT.diagonalization (T v) μ = (μ : 𝕜) • hT.diagonalization v μ

---

• depends on: [Merged by Bors] - feat(analysis/inner_product_space/rayleigh): Rayleigh quotient produces eigenvectors #9840
• depends on: [Merged by Bors] - feat(analysis/normed_space/pi_Lp): use typeclass inference for 1 ≤ p #9922
• depends on: [Merged by Bors] - chore(algebra/module/submodule_lattice): lemmas about the trivial submodule #10022
• depends on: [Merged by Bors] - feat(linear_algebra/eigenspace): define eigenvalues of an endomorphism #10027

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(analysis/inner_product_space/rayleigh): Rayleigh quotient produces eigenvectors #9840
• [Merged by Bors] - feat(analysis/normed_space/pi_Lp): use typeclass inference for 1 ≤ p #9922
• [Merged by Bors] - chore(algebra/module/submodule_lattice): lemmas about the trivial submodule #10022
• [Merged by Bors] - feat(linear_algebra/eigenspace): define eigenvalues of an endomorphism #10027

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[ocfnash]

A few nits but otherwise this looks great.

bors d+

I do have one question though: the main results here hold with the weaker assumption that E is complete rather than finite-dimensional. Is there a reason not just to go straight for the stronger versions?

[ocfnash]

Can this convert be avoided? Is it some annoying decidability typeclass issue that renders it necessary?

[hrmacbeth]

Yes -- I would love to know how to fix it!

[ocfnash]

The need for by convert is indeed due to two different decidability typeclasses, one classical, one not.

To be precise if you add [decidable_eq ι] to the lemma orthogonal_family.submodule_is_internal_iff then you can drop the by convert here.

I believe that you should add [decidable_eq ι] as an argument to orthogonal_family.submodule_is_internal_iff and also add [decidable_eq 𝕜] as an argument here (i.e., to direct_sum_submodule_is_internal) because otherwise these lemmas contain classical decidability instances (which is a Bad Thing).

Maybe @eric-wieser could confirm / refute my claims given his recent helpful words on Zulip

[hrmacbeth]

To be precise if you add [decidable_eq ι] to the lemma orthogonal_family.submodule_is_internal_iff then you can drop the by convert here.

Indeed. Thank you!!

I believe that you should ... also add [decidable_eq 𝕜] as an argument here (i.e., to direct_sum_submodule_is_internal)

Should I also add [decidable_eq 𝕜] as an argument to orthogonal_family.submodule_is_internal_iff? Or only here?

[ocfnash]

I defer to a true decidability expert.

I think the way I would settle this is to remove open_locale classical (I recommend never using it) and see what decidability assumptions you then need to add to make the statements of your lemmas typecheck. And of course if any proofs break just invoke the classical tactic.

[hrmacbeth]

OK, removed classical from projection.lean and spectrum.lean!

[bors]

✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[hrmacbeth]

I do have one question though: the main results here hold with the weaker assumption that E is complete rather than finite-dimensional. Is there a reason not just to go straight for the stronger versions?

What do you mean exactly? If you're talking about the result for compact operators, I believe I need to define compact operators and also define and write an API for the Hilbert sum of an (infinite) family of inner product spaces. But I'm heading there :). Is there another version you have in mind?

[ocfnash]

I do have one question though: the main results here hold with the weaker assumption that E is complete rather than finite-dimensional. Is there a reason not just to go straight for the stronger versions?

What do you mean exactly? If you're talking about the result for compact operators, I believe I need to define compact operators and also define and write an API for the Hilbert sum of an (infinite) family of inner product spaces. But I'm heading there :). Is there another version you have in mind?

Good clarification, I should indeed have said "with the weaker assumption that E is complete and T is compact" (both of which are automatic in finite dimensions). I was just dusting off some very old thoughts and IIRC you don't need to use the finite-dimensional spectral theorem to get the infinite-dimensional one. If that's true then there's no need to start out with the finite-dimensional case.

[hrmacbeth]

IIRC you don't need to use the finite-dimensional spectral theorem to get the infinite-dimensional one. If that's true then there's no need to start out with the finite-dimensional case.

There's quite a bit of infrastructure needed for the infinite-dimensional case (the Hilbert sum API in particular). So I think we'll want this more elementary finite-dimensional version which uses pi_Lp (rather than the Hilbert sum) anyway, to reduce the imports needed when someone wants just the finite-dimensional version. Since I expect writing the Hilbert sum API to be a big project, I also wanted a bit of quick gratification first in finishing off the finite-dimensional version :)

But I have been bearing the infinite-dimensional version in mind when structuring this file: did you notice that everything down to

lemma orthogonal_supr_eigenspaces (μ : 𝕜) :
  eigenspace (T.restrict hT.orthogonal_supr_eigenspaces_invariant) μ = ⊥ :

in this file and everything down to

lemma has_eigenvector_of_is_max_on (hT : is_self_adjoint (T : E →ₗ[𝕜] E)) {x₀ : E}
  (hx₀ : x₀ ≠ 0) (hextr : is_max_on T.re_apply_inner_self (sphere (0:E) ∥x₀∥) x₀) :
  has_eigenvector (T : E →ₗ[𝕜] E) ↑(⨆ x : {x : E // x ≠ 0}, rayleigh_quotient x) x₀ :=

in the Rayleigh file has no [finite_dimensional 𝕜 E] assumption?

We can talk more on Zulip if you're curious about the approach.

[ocfnash]

There's quite a bit of infrastructure needed for the infinite-dimensional case ... I also wanted a bit of quick gratification first in finishing off the finite-dimensional version :)

Totally agreed, and indeed this is already a very useful and gratifying result! I especially agree about the point about needing a findim version that does not invoke the infdim direct sum machinery etc.

But I have been bearing the infinite-dimensional version in mind when structuring this file: did you notice that everything down to ... and ... has no [finite_dimensional 𝕜 E] assumption?

I did notice this!

We can talk more on Zulip if you're curious about the approach.

I have no more questions but I'm always happy to chat!

[hrmacbeth]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests