Real multiplication

[lowasser]

I'm doing some travel with only a Chromebook that can run VSCode and at least edit Agda with all the symbols etc, but doesn't have the capacity (RAM?) to compile unimath, choking on foundation-core.commuting-squares-of-maps AFAICT. I might figure out a solution later, but my ability to do new development is limited, and I don't want to do every step of development by pushing drafts to this repository and waiting for make check, so I'm dumping notes here.

To accomplish real multiplication, we need:

1. Minimum and maximum on the rational numbers. (Both Minimum and maximum on the lower, upper, and usual Dedekind real numbers #1335 and Multiplication on closed intervals of rational numbers #1351 include this.)
2. Negative and nonnegative rational numbers. (We can probably get away without nonpositive rational numbers, but we should arguably do at least a basic job on them for completeness' sake...)
3. The absolute value on rational numbers and many of its properties. (These generally follow from the first two.) Nonnegativity, multiplicativity, triangle inequality...the connection with the metric space of rational numbers doesn't hurt, but since that's defined on positive distances only, it's not quite the same thing as absolute values of differences. Though we can probably get the triangle inequality on the metric space from the triangle inequality on absolute values, if not the other way around.
4. Multiplication on closed intervals of rational numbers #1351 to bound multiplication on closed rational intervals.
5. Arithmetic locatedness of real numbers (currently part of Addition on real numbers #1336)
6. Absolute value on real numbers (depends on Minimum and maximum on the lower, upper, and usual Dedekind real numbers #1335). As usual in constructive settings, abs-R x is max x (neg-R x).

The definition of multiplication on Dedekind cuts from HoTT becomes not too terrible after this. Dumping the math here for funsies:

q is in the lower cut of x * y if there are rational bounds on x and y: a < x < b, c < y < d, such that q is less than the minimum of ac,ad,bc,bd, and correspondingly for the upper cut (greater than the maximum).

Inhabitedness is easy: pick any bounds (inhabitedness of the lower and upper cuts of x and y), and pick a lesser (greater) value.
Roundedness is easy: no need to change the bounds, just pick the mediant of q and the minimum (maximum) of the products of the rational bounds.
Disjointness follows from #1351: given any two different rational bounds a b c d and a' b' c' d', you can show the minimum of the products of a b c d is less than or equal to the maximum of the products of a' b' c' d' by showing max a a' * max c c' is a product of elements in both closed intervals [a,b]*[c,d] and [a',b']*[c',d'], so the lower bound from the first is at most the upper bound from the second. Therefore if q is less than lower bound from a b c d and greater than the upper bound from a' b' c' d', it is less than itself, contradiction.
Locatedness follows from arithmetic locatedness. To approximate xy within epsilon, first pick rational p > abs-R x and q > abs-R y (inhabitedness of the upper cut of the absolute value). Pick positive rationals delta < min(1 , eps/2 * inv-Q+ (q + 1)), theta < min(1 , eps/2 * inv-Q+ (p + 1)). (Division by 2 not actually required; left- and right-summand-split-Q+ suffices.) Using arithmetic location on x and y, pick a < x < a + delta and b < y < b + theta. Then

|(a+delta)(b+theta) - ab| 
<= |theta*a + delta*b + delta*theta| 
<= theta|a+delta| + delta|b| 
<= theta|a+1| + delta|b+1|
< theta*(p+1) + delta(q+1) <= eps2 + eps1 = epsilon

I suppose it takes a few more steps to quite get the results we want -- we have to take the minimum on all of ab,a(b+theta),(a+delta)b,(a+delta)(b+theta), and we need strict bounds on the minimum and maximum, not the minimum and maximum themselves, but that seems like it will get the job done.

That adds up to a pretty big project, but not one that's bigger (or at least significantly bigger) than real addition has been.