feat(analysis/inner_product_space/positive): Positivity of linear maps

[themathqueen]

this pr

• defines positivity of a linear map
• proves a positive linear map has a nonnegative spectrum

---

• depends on: [Merged by Bors] - feat(analysis/inner_product_space/basic): orthogonal submodules #18705
• depends on: [Merged by Bors] - refactor(analysis/inner_product_space): split submodule.orthogonal to a new file #18706

[YaelDillies]

The name of this PR is very undescriptive. Can you improve it?

[ADedecker]

I feel bad to tell you this after you've done all this work, but I don't think we want this definition (or rather, we want it in a much more general context, so this will likely get removed in the future when we are able to state the general version).
We will soon have the continuous functional calculus in mathlib (see #17164) which is the first step for making this definition in the general setup (although there is some work needed to show that positivity implies positivity of the spectrum, but in the case of continuous linear maps this is doable). Then of course we will need to know how it works in this concrete setup, but it seems wrong to do so much work with this restricted definition.
@j-loreaux what is your opinion on this?

[j-loreaux]

I'm not sure how I missed this ping (EDIT: figured it out, I started a review but never finished it). Anatole is correct that this can easily† be achieved with the continuous functional calculus. When that happens there will be a general sqrt that can be used on the appropriate maps. In particular, the sqrt function I'm imaging will be defined on elements of the positive cone of a (possibly non-unital) star_ordered_ring whenever we have the continuous functional calculus. If you want to apply this to a continuous_linear_map, you'll just need to do what Anatole suggested and prove that positivity (in terms of the inner product) implies positivity of the spectrum.

†this is perhaps a gross overstatement of the simplicity of this task. It's not as trivial as just popping in continuous_functional_calculus and going off to the races. I need to develop an entire API for the continuous functional calculus, and in particular it is vitally important that we get the non-unital version in before we really start to use it (I can explain, but I won't for now). I have started to develop this API on a branch, but it's not ready for prime time yet, and it probably won't be until after the port.

[YaelDillies]

Let me remark that those results pertain to the theory of C*-algebras.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(analysis/inner_product_space/basic): orthogonal submodules #18705
• [Merged by Bors] - refactor(analysis/inner_product_space): split submodule.orthogonal to a new file #18706
  By Dependent Issues (🤖). Happy coding!

[mcdoll]

I don't understand why Anatole's remark is completely ignored. The continuous functional calculus is in mathlib, so the easy way to prove things about positive operators is to use that. The change of the positivity definition seems to make it harder to connect these two parts of mathlib, imo.

[eric-wieser]

I don't understand why Anatole's remark is completely ignored.

I skim-read it as "don't define sqrt, it's not needed", and sqrt has now been removed. It sounds like you're able to read more into the remark than I am.
Perhaps the best approach is to see what @ADedecker thinks about the current state.

[kim-em]

I don't like the name here. It should to something like to_linear_map_is_positive_iff?

[kim-em]

Would this be nicer if we had two separate is_positives, in linear_map and in continuous_linear_map?

[eric-wieser]

Would this be nicer if we had two separate is_positives, in linear_map and in continuous_linear_map?

I suggested in a previous comment that it would be nice to merge the two definitions so that we didn't have to duplicate a handful of lemmas between the two cases.

[j-loreaux]

One thing to note here: I'm not sure how valuable an is_positive definition and API are going to be. Ultimately, I think we'll want to take everything through something that doesn't exist yet: the positive cone in a star_ordered_ring, because this will (eventually) be the thing that has access to all the nice API (like the continuous functional calculus). I'm not necessarily saying we should abandon this PR, only that we may want to postpone it; I realize it's been sitting for a long time already.

[kim-em]

I've created a zulip thread about this PR.

[j-loreaux]

Per this Zulip discussion, this PR won't be merged (at least not in this form), but we are keeping it open as a reminder that some of these results don't yet exist in mathlib and that we are just taking a different approach.