feat: show some convexity properties of intervals

[kilianar]

Add some basic results about convexity of intervals in ordered semirings. The statements are somewhat asymmetric because, in this level of generality, the convex hull of two points need not coincide with the interval between them.

[martinwintermath]

What is the mathematical story here? I see

• "convex hull of {a,b} is in Icc a b", but not the other inclusion
• "Icc 0 1 is in convex hull of {0, 1}", but not for general a,b

Why these restrictions? And when can they be lifted?

[YaelDillies]

The question is when x <= y <= z implies that there exist a, b nonnegative summing to 1 such that ax + bz = y. When x = 0, z = 1, ExistsAddOfLE is enough (and is more or less equivalent to it). For general x and z, you probably need to divide, i.e. you need a semifield.

[martinwintermath]

The question is when x <= y <= z implies that there exist a, b nonnegative summing to 1 such that ax + bz = y. When x = 0, z = 1, ExistsAddOfLE is enough (and is more or less equivalent to it). For general x and z, you probably need to divide, i.e. you need a semifield.

So ideally this PR adds the respective equality lemmas under Semifield assumptions.

[kilianar]

Yes, I think one can show the equality for arbitrary $a,b$ in a semifield. I will try to do so.

For a general ordered convex space $X$, however, we only get $\mathop{\mathrm{convHull}} \{a,b\} \subseteq [a,b]$, and equality need not hold. For example, in $X=\mathbb{R}^2$ with the coordinatewise order, for $a=(0,0)$ and $b=(1,1)$, the convex hull is the diagonal segment, while $[a,b]$ is the whole unit square.

[martinwintermath]

LGTM @ooovi
@YaelDillies: is there any unfinished discussion regarding IsOrderedConvexSpace or so that we should wait for?

[YaelDillies]

Yes, let's wait for the IsOrderedConvexSpace R R assumption to be gone