Strong positivity

Stream: general

[Eric Wieser]

Jeremy Avigad said:

With my American undergraduate and graduate training in mathematics, I interpret "x is positive" as "x > 0." Webster agrees with me:
https://www.merriam-webster.com/dictionary/positive
Wikipedia lists both interpretations:
https://en.wikipedia.org/wiki/Sign_(mathematics)#Terminology_for_signs

From that second page:

The same terminology is sometimes used for functions that yield real or other signed values. For example, a function would be called a positive function if its values are positive for all arguments of its domain, or a non-negative function if all of its values are non-negative.

Which is already not what 0 < f means in Mathlib!

[Yury G. Kudryashov]

BTW, sometimes ∀ x, f x < g x is the right notion (e.g., if we want to generalize docs#isOpen_Ioi)

[Yury G. Kudryashov]

But I don't know how to formulate it in terms of a PartialOrder.

[Yaël Dillies]

docs#Pi.StrongLT

[Anatole Dedecker]

It’s just docs#StrongLT apparently

[Yury G. Kudryashov]

Anatole Dedecker said:

It’s just docs#StrongLT apparently

But we don't have a generic StrongLT that works for linear orders, Prods and Pis of them.

[Yaël Dillies]

Yeah, I thought about this problem, but haven't come up with a solution yet.

[Eric Wieser]

Is the solution not to make StrongLT a type class?

[Jireh Loreaux]

There's more annoyances too in the realm of strongly positive. In C star algebra theory an element a is said to be strictly positive if it is positive (i.e., 0 \le a) and the hereditary C star subalgebra it generates is the full algebra. If you represent that C star algebra faithfully on a Hilbert space, that condition is that the element corresponding to a is positive and zero is not an eigenvalue (or equivalently, for all x, 0 < inner (a x) x), which is the link to strongly positive.

[Yaël Dillies]

Eric Wieser said:

Is the solution not to make StrongLT a type class?

If it were a typeclass, we would still need to state something about it. Else it's just notation.

[Yaël Dillies]

In particular, what should StrongLT mean on alpha x beta x gamma? With the obvious definition, it would mean x.1 < y.1 and (x.2.1 < y.2.1 and x.2.2 <= y.2.2 or x.2.1 <= y.2.1 and x.2.2 < y.2.2, which is not the same as x.1 < y.1 and x.2.1 < y.2.1 and x.2.2 < y.2.2.
One solution would be to have an instance LinearOrder alpha -> StrongLT alpha and then the instance StrongLT alpha -> StrongLT beta -> StrongLT (alpha x beta).

[Notification Bot]

13 messages were moved here from #general > RFC: naming convention for nonneg/pos by Eric Wieser.