Positive operators

Stream: maths

[Moritz Doll]

A bit of a bikeshedding thing, but I am not entirely sure, whether the naming of positive operators in inner_product_space is good. The literature uses both non-negative and positive for the condition is_self_adjoint and $\langle Ax, x\rangle \geq 0$. A major reason for using positive is that the spectrum is closed so the condition $\langle Ax, x\rangle > 0$ is not used that often. On the other hand having nonneg would be more consistent with the rest of mathlib and saying that the zero operator is positive also sounds a bit weird.
@Heather Macbeth @Anatole Dedecker

[Scott Morrison]

There's tension between consistency with mathematical usage, and uniformity in naming. I'm inclined to use positive here.

[Frédéric Dupuis]

I would vote for nonneg -- when searching for a lemma in the context of mathlib this is definitely what I would try first!

[Jireh Loreaux]

This is a tough one in my opinion. I'm leaning towards nonneg because I have always felt this concept was misnamed.

Is this in the inner_product_space namespace?

[Kalle Kytölä]

The term "positive" is more succinct than nonnegative, and is indeed (ab)used in math quite a lot.

In mathlib, there is already for example docs#measure_theory.Lp.pos_part and docs#measure_theory.Lp.neg_part. I don't think I would like to decompose a function to its "nonnegative part" and the "nonpositive part".

This is a tradeoff between accuracy and simplicity of terminology. I'd prefer to compromise on the accuracy. But I can understand the opposite preference, too.

Either way, consistency within mathlib has value, for example when searching.

[Jireh Loreaux]

By the way, strictly positive operators do come up, and it would be a shame to have to call them strictly positive just because positive is already taken.

[Kalle Kytölä]

Ok, in this case it is a difficult choice and I don't have a strong opinion.

But yet another context in which it is extremely standard to abuse terminology is "positive linear functionals". I have never heard people call them "nonnegative linear functionals". So at least in many situations, I would prefer to allow the usual abuse of terminology.

[Moritz Doll]

Jireh Loreaux said:

This is a tough one in my opinion. I'm leaning towards nonneg because I have always felt this concept was misnamed.

Is this in the inner_product_space namespace?

It's in continuous_linear_map to allow for dot-notation. As I mentioned in https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315326.20Renaming.20is_self_adjoint/near/290904416 one could make it a subtype of an abstract star_ring, but that would require serious work to prove that the abstract definition is equivalent to the current one.

[Anatole Dedecker]

I have to say that nonnegative_operator would seem really weird to me, not only because I’m French, but because « nonnegative » would not mean « not negative » in this case…

[Anatole Dedecker]

I know English people are used to this kind of thing (« nonincreasing » for example), but that seems really weird to me

[Sebastien Gouezel]

nonnegative really means "positif ou nul", so I don't think there is any problem here, you just have to get used to it. And yes, English people are crazy :-)

[Jireh Loreaux]

I think "nonnegative" here means "not anywhere negative"

[Moritz Doll]

I always read it as non-negative spectrum

[Jireh Loreaux]

I guess I can live with the fact that English people are crazy; I'm American anyway. :joy:

[Yaël Dillies]

Yeah... "nonnegative" only really makes sense in linear orders. I much prefer the French convention here.

[Junyan Xu]

maybe "semipositive" as a shorthand for positive semidefinite.

[Heather Macbeth]

I always vote for going with pre-existing mathematical terminology, even when it breaks mathlib consistency a little.

[Frédéric Dupuis]

"Nonnegative operator" is used quite a bit in the literature actually even if it's not the dominant term, so it wouldn't be a radical move.

[Sebastien Gouezel]

Wikipedia uses "positive-semidefinite" or "nonnegative".

[Moritz Doll]

I've never gotten weird looks for using "nonnegative" in talks, people are more confused that my Laplacian is nonnegative :grinning:

[Sebastien Gouezel]

Of course Laplacian is nonnegative! (according to 80% mathematicians as far as I can tell, but it might depend on communities :-)