feat(analysis/inner_product_space/sqrt): is_self_adjoint.sqrt

[hparshall]

We define the square root of a self-adjoint operator T on a
finite-dimensional inner product space E in terms of an orthonormal
basis of eigenvectors for T.

Once analysis.inner_product_space.spectrum contains spectral theory
for bounded operators, we can generalize to bounded self-adjoint
operators. In the meantime, this finite-dimensional result will be
useful for polar and singular value decompositions.

Co-authored-by: Daniel Packer

---

[dupuisf]

I'm a bit reluctant to merge this, since we'll get a much more general construction allowing to do this soon(ish): the continuous functional calculus, which will let us apply continuous functions to elements of a C*-algebra. It might be OK as a temporary measure if it's really blocking things we want (do you have code that depends on this lined up?), but I'd like to avoid getting in too deep.

[hparshall]

I'm a bit reluctant to merge this, since we'll get a much more general construction allowing to do this soon(ish): the continuous functional calculus, which will let us apply continuous functions to elements of a C*-algebra. It might be OK as a temporary measure if it's really blocking things we want (do you have code that depends on this lined up?), but I'd like to avoid getting in too deep.

I understand this reluctance given the bright functional future! I thought this might be a bit specific. We do have some code for polar decomposition & SVD that we're cleaning up and contributing that depends on this. I don't know how pressing our formulations of these are; we are most interested in the finite-dimensional situation, and so some of our code has needed generalization.

Happy to clean it up to get it in, but also totally understand if it isn't helpful at this time.

[hrmacbeth]

Independent of the point raised by @dupuisf, I'd like to suggest that if this construction is kept that it's proved in a more canonical way: you can use the splitting into eigenspaces (the "first version" of the spectral theorem in the current library) rather than the further splitting by choosing a subordinate basis for that eigenspace.

[jcommelin]

@hparshall What do you think of Heather's comment above?

[hparshall]

Independent of the point raised by @dupuisf, I'd like to suggest that if this construction is kept that it's proved in a more canonical way: you can use the splitting into eigenspaces (the "first version" of the spectral theorem in the current library) rather than the further splitting by choosing a subordinate basis for that eigenspace.

This seems like a reasonable suggestion that I will follow up on.