!3#18230 Positivity of linear maps

Stream: PR reviews

[Scott Morrison]

@Monica Omar, @Jireh Loreaux. I propose we close !3#18230, or otherwise remove it from the not-too-late list for mathlib3. My reading of the conversation there was that we were far from certain whether we wanted these definitions in mathlib. As such maybe it makes sense that anything that grows out of this PR should happen directly in Mathlib4?

I'm very happy to be corrected here and to have further discussion about this PR. If we do decide not to proceed with it, I'm very sorry @Monica Omar for how long this has taken. Unfortunately everyone's attention has been diverted by the porting process, and many PRs languished unreasonably long on the #queue3.

[Jireh Loreaux]

Yeah, I think removing it from the the not-too-late list or closing is the right approach for now (sorry Monica!). I'm not against having the predicate so much as I am against developing the API around that predicate. For reference, my plan for positivity is #4871. Then we can have TFAEs which give equivalent conditions in certain contexts (like IsPositive, or that the spectrum is nonnegative).

[Anatole Dedecker]

I would also like to apologize since I started reviewing this but then disapeared and let it rot, and I'm really glad to see that this hasn't discouraged Monica to contribute to Mathlib.

[Anatole Dedecker]

My views on this positivity predicate have also evolved (I was the one introducing docs#ContinuousLinear.IsPositive after all!) and I now think that the correct way to do this is to have one notion, which is positivity in C*-algebras (actually in star rings with assumptions that I don't knpw) and then multiple ways to characterize for specific algebras. This used to be a long-term ideal, but now that it's just around the corner I think this PR goes a bit in the wrong direction, and indeed some of the existing API around positive continuous linear maps should probably go as well.

[Anatole Dedecker]

Probably this PR can stay open though, as a reminder that some of these result still don't exist in Mathlib and that we are just taking a different approach.

[Monica Omar]

Jireh Loreaux said:

Yeah, I think removing it from the the not-too-late list or closing is the right approach for now (sorry Monica!). I'm not against having the predicate so much as I am against developing the API around that predicate. For reference, my plan for positivity is #4871. Then we can have TFAEs which give equivalent conditions in certain contexts (like IsPositive, or that the spectrum is nonnegative).

Hmm, I see your point. I'm not sure I'm entirely convinced, though. For linear maps, I feel like you should only define positivity (or non-negativity) 0 ≤ x for symmetric linear maps x and not just for any linear map.

[Jireh Loreaux]

Do you mean only define it for the subtype (e.g., selfAdjoint A)? Or do you mean that positivity should imply IsSymmetric? If the former, then I don't agree (because it's just inconvenient), and I can explain further if you want. If the latter, then of course I agree, but that is already entailed by my definition.

[Monica Omar]

Inconvenient in what sense?

[Jireh Loreaux]

You have a subtype of a subtype (in general, yuck to that), and then you have to apply two Subtype.val coercions to get to the full type. It also prevents you from being able to talk about x ≤ y for arbitrary x y : A, which is inconvenient because it means you would need to build terms of type selfAdjoint A first. Generally, requiring fewer hypotheses makes life easier (think of junk values, for example). And in this case, x ≤ y is actually meaningful for x y : A anyway: it means 0 ≤ y - x (and necessarily y - x is self adjoint here, but that's effectively a theorem, not a hypothesis you have to check).

I used to think we should only have ≤ on the selfAdjoint A subtype, but I've been converted. :smiley:

[Jireh Loreaux]

PSA: I removed the not-too-late tag but left the PR open since that seemed to be the consensus.

[Monica Omar]

Yeah, actually, you're completely right! I see your point now haha. On paper, it seems fine to define it that way; but in Lean it gets messy.

Well, shouldn't we just remove the definition of positive continuous linear maps now then? And make a theorem for the inner product being non-negative for positive maps. Same goes for matrices, instead of having the positive semi-definite definition, we should probably just remove it now and make that as a theorem?

[Anatole Dedecker]

That’s probably the end goal indeed. That said, there’s no point in removing something until we have the better alternative (in the same way that there is no point in adding something that will be refactored): the most sane thing to do is to just not touch it until we have the better solution available.

[Eric Wieser]

An argument in favor of 18230 is that it just generalizes the is_positive we already have to work for linear_maps too

[Monica Omar]

Yeah, that is true! So, in a sense, it's not going in the wrong direction, it's just keeping the same definition, but making it work for more stuff

[Anatole Dedecker]

Yes but we’ll want to remove that at some point so there’s no point generalizing it.

[Monica Omar]

But we can add a lot more results by generalizing it or changing the definition to something better. And the results would only need to be slightly changed after removing the definition.

[Anatole Dedecker]

Thinking about it, won’t we run into some trouble because the space of linear maps is not a star algebra? For the same reason that we have docs#LinearMap.IsSymmetric as well as the general docs#IsSelfAdjoint

[Anatole Dedecker]

Monica Omar said:

But we can add a lot more results by generalizing it or changing the definition to something better. And the results would only need to be slightly changed after removing the definition.

I’m not sure I follow you. Do you agree that the ideal definition (modulo the possible issue I just posted about) is the one for star algebras?

[Monica Omar]

Yeah, I agree, that is the ideal definition. I meant that, for the meantime, couldn't we change positivity for continuous linear maps to: x is positive if there exists y such that x = star y * y? I feel like that is a way forward, at the moment.

[Monica Omar]

Anatole Dedecker said:

Thinking about it, won’t we run into some trouble because the space of linear maps is not a star algebra? For the same reason that we have docs#LinearMap.IsSymmetric as well as the general docs#IsSelfAdjoint

That's a fair point. So we won't be able to define positivity for linear maps then? Doesn't that mean that we should have the definition in this PR?

[Anatole Dedecker]

I don’t know enough about the theory of partial operators, but I’m sure Moritz can tell us if we have a way around that. In particular, does it help if we extend to docs#LinearPMap ? It is true that symmetric linear maps are exactly those which are equal to their adjoint as LinearPMaps, right?

[Anatole Dedecker]

Monica Omar said:

Yeah, I agree, that is the ideal definition. I meant that, for the meantime, couldn't we change positivity for continuous linear maps to: x is positive if there exists y such that x = star y * y? I feel like that is a way forward, at the moment.

Ah yes that might be an interesting temporary step. In particular, we'll have to prove that this characterization is equivalent to the current definition at some point, and that can probably be done without having the fully general setup as long as we make sure that the new definition we choose is exactly the one we'll use in the general case
EDIT: changed my mind

[Anatole Dedecker]

That said, I’m not sure you’ll be able to prove it conveniently without more API for the continuous functional calculus (to define the square root)

[Eric Wieser]

Isn't that the meaning used by docs#StarOrderedRing ?

[Monica Omar]

I don't think we should define the square root at the moment. But, I think having star y * y be the new definition for positivity of continuous linear maps is as close as we can currently get to positivity for general star algebras

[Monica Omar]

Also, yeah, having star y * y be the new definition also means we can define a partial order on the set of continuous linear maps, and then we can get a star ordered ring. I feel this is very useful.

[Eric Wieser]

You probably want the more general x ≤ y := ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p that we use in StarOrderedRing

[Monica Omar]

We can then remove the definition of positive semi-definite-ness for matrices and use the same definition. So this makes things a lot nicer

[Monica Omar]

Do y'all agree? Should I do this?

[Anatole Dedecker]

Anatole Dedecker said:

Monica Omar said:

Yeah, I agree, that is the ideal definition. I meant that, for the meantime, couldn't we change positivity for continuous linear maps to: x is positive if there exists y such that x = star y * y? I feel like that is a way forward, at the moment.

Ah yes that might be an interesting temporary step. In particular, we'll have to prove that this characterization is equivalent to the current definition at some point, and that can probably be done without having the fully general setup as long as we make sure that the new definition we choose is exactly the one we'll use in the general case

Sorry, this message was a bit silly, The whole point of waiting for Jireh's work on continuous functional calculus is to be able to prove this equivalence in a nice way, and his PR #4871 already contains a good basis for the details of this definition. I think we should switch the focus on making sure that the setup in #4871 is nice enough before going any further, and I fear that any attempt to skip steps here will only make our lives harder.

[Monica Omar]

I don't get it. How are we going to have a partial order if we don't have a definition for positivity?

[Monica Omar]

Like what exactly is the plan after #4871?

[Anatole Dedecker]

Ah yes I misinterpreted the content of this PR. To be honest I'm not 100% happy with the proposed plan either, but my point is that we should focus our efforts here. You are very much welcome to participate in the discussions though, but we should really do it one step at a time and I worry that we end up with an unusable API if we do too much things in parallel without proper discussion.

[Monica Omar]

Yeah, I agree, open communication is very important. We need to openly communicate our plans instead of impulsively doing things and having unusable API.

[Notification Bot]

35 messages were moved from this topic to #PR reviews > #4871 StarOrderedRing.positive by Jireh Loreaux.