complex order

Stream: maths

[Yury G. Kudryashov]

I've just realized that assumption h₂ : 0 < (f x).re ∨ (f x).im ≠ 0 of docs#has_deriv_at.clog and a bunch of similar lemmas can be formulated as ¬ (f x ≤ 0) in locale complex_order, see docs#complex.complex_partial_order and its redefinition in #9420. Why not make it an instance?

[Johan Commelin]

I think it was/is controversial to make that order an instance on ℂ, because it is pretty non-canonical.

[Johan Commelin]

We should probably add some comments about the pros and cons to one of those files.

[Yury G. Kudryashov]

Another solution: define it as an instance, add a library note, and mention it in the docstring of every lemma that depends on complex.partial_order.

[Yury G. Kudryashov]

I guess, we can have a linter for the docstring requirement.

[Johan Commelin]

I think @Scott Morrison was one of the proponents of making this an instance. But maybe I don't remember correctly.

[Scott Morrison]

In any Banach algebra, there's the cone of positive elements. Everyone would be pretty happy saying that there is a partial order on the self-adjoint elements, given by x >= y iff x - y is positive. Of course, you can extend that definition to the whole Banach algebra if you like: x and y will never be comparable if their difference is not self-adjoint. Is that a useful thing to do? Not obvious. Yury is observing that it's ever so slightly useful for stating some hypotheses concisely.

I'm still in favour of making it an instance, on the general theme that we like to make our functions "total", and so we might as well extend the partial order of self-adjoint elements to a partial order on everything, using "the default value" of "incomparable". But I agree that not everyone is going to like that -7 + 7i < 1 + 7i.

[Johan Commelin]

I'm complex-partial-order-agnostic.

[Scott Morrison]

Yury has a PR that puts the instances in a locale complex_order, which seems a good middle path.

[Kevin Buzzard]

0<re or im!=0 is instantly comprehensible to any reader, whereas not z<=0 is instantly confusing

[Kevin Buzzard]

I should add that it's not just experts who read mathlib. I sometimes link to mathlib code on Twitter for example as part of my evangelism attempts

[Yury G. Kudryashov]

They were already in this locale. I'm changing the definition from ∃ x : real, 0 ≤ x ∧ z + x = w to something about re and im.