Add maximum of two real numbers to iset.mm

[jkingdon]

The goal is to define max(x,y) such that it is the larger of x or y. Since the obvious way of defining this relies on real number trichotomy, it may be surprising to hear that max can be defined without excluded middle.

One way relies on the Dedekind cut construction, where we define a cut whose lower cut is the union of the lower cuts of x and y, and the upper cut is the intersection of the upper cuts of x and y.

The other way should not require any new real number axioms and defines max in terms of ax-caucvg. It is described in Definition 3.7 of http://us.metamath.org/ileuni/mmil.html#Geuvers

The properties we expect of max are Lemma 3.8, Lemma 3.9, Lemma 3.10, Lemma 3.11, Lemma 3.12

max is also mentioned, much more briefly, in Definition 11.2.7 of http://us.metamath.org/ileuni/mmil.html#HoTT

As an aside, real absolute value can be defined in terms of max (Definition 3.13 of Geuvers). However, we might want to go directly to complex absolute value as in http://us.metamath.org/mpeuni/df-abs.html

[benjub]

I haven't looked at the references, but the following definitions look pretty simple:

abs(x) := sqrt(x^2) max(x,y) := (x + y + abs(x - y)) / 2

[jkingdon]

I haven't looked at the references, but the following definitions look pretty simple:

abs(x) := sqrt(x^2) max(x,y) := (x + y + abs(x - y)) / 2

Oooh, cool. The references define max first, before square root. But if we define square root first, then it looks like the above definition will be way easier than the Dedekind cut or Cauchy sequence approach.

[david-a-wheeler]

I think those definitions make sense. However, they're different than many other definitions.

If they're used in iset.mm, I recommend including a discussion in the definitions of iset.mm to explain why these definitions are used (and not other ones). Also, I'm hoping that there will be many theorems proven that prove the same results as set.mm, even if the underlying definitions are slightly different, so that other set.mm theorems can be easily used. Bonus round: show, in set.mm, that the definitions are equivalent in classical logic :-).

[digama0]

I don't think we should worry about differing definitions in iset.mm at all. This will be frequently required. In any case, what is required from the function is that max(a, b) = b when a <= b and max(a, b) = a when b <= a, and these are of course true for both the set.mm and iset.mm max functions. (The main annoying bit is that set.mm doesn't actually define a max function, it just uses if ( A <_ B , B , A ), so a lot of the theorems about max are just if theorems with names to match.)

[jkingdon]

I think those definitions make sense. However, they're different than many other definitions.

A definition like the one implicit in http://us.metamath.org/mpeuni/max2.html is based on real number trichotomy (it doesn't really make sense unless A <_ B \/ B <_ A which is a theorem that iset.mm only has for rationals or integers, but cannot have for reals).

Also, I'm hoping that there will be many theorems proven that prove the same results as set.mm

Would be more graceful if set.mm had a notation for max. I also don't know if set.mm has the theorems discussed here - Lemma 3.8, Lemma 3.9, Lemma 3.10, Lemma 3.11, Lemma 3.12 of [Geuvers] (the "what is required" theorem mentioned by @digama0 is Lemma 3.12, well combined with Lemma 3.9 which says that max(x,y) = max(y,x)).

[david-a-wheeler]

Would be more graceful if set.mm had a notation for max.

That doesn't sound too hard :-).

[benjub]

I think there is no need for a new token for the maximum of two real numbers: it is too specific a construction, and not much is gained compared to

sup ( { A , B } , RR , < )

Is the sup defined in iset.mm ? Then, my definition in the comment above becomes a theorem:

$p |- ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) = sup ( { A , B } , RR , < ) ) $= ? $.

(to be written in deduction form, maybe).

By the way: to @digama0's two conditions

a <= b -> max(a, b) = b b <= a -> max(a, b) = a

one should add the third condition

( a <= c /\ b <= c ) -> max(a, b) <= c

which is necessary for a characterization since intuitionistically, we do not have ( a <= b \/ b <= a ) for reals. Actually, Mario's two conditions should ideally be deduced from that third condition together with the two conditions

a <= max(a , b) b <= max(a , b)

which are more fundamental and make the max appear as a sup. (Of course, all these conditions being formulated in iset.mm using the expression sup ( { A , B } , RR , < ) ).

[jkingdon]

sup ( { A , B } , RR , < )

Oooh nice. I think this might work (it isn't as self evident as in set.mm but if you look at the supremum theorems recently added in iset.mm including the recent ones for greatest common divisor, it perhaps seems intuitive this may be possible).

If no one beats me to it, I may start looking at this once I'm done with #2374

[benjub]

sup ( { A , B } , RR , < )

Oooh nice. I think this might work (it isn't as self evident as in set.mm

It is not ! The hard part is the theorem I proposed above. The idea is to prove

|- ( ( A e. RR /\ B e. RR ) -> A <_ sup ( { A , B } , RR , < ) )

(and since { A , B } = { B , A }, you obtain the other one), and

|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < C /\ B < C ) ) -> sup ( { A , B } , RR , < ) <_ C )

From these three theorems, prove

|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> sup ( { A , B } , RR , < ) = B ) ) |- ( ( A e. RR /\ B e. RR ) -> ( B < A -> sup ( { A , B } , RR , < ) = A ) )

as well as the hard one:

$p |- ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) = sup ( { A , B } , RR , < ) ) $= ? $.

Good luck @jkingdon !

[jkingdon]

as well as the hard one

Yeah, the hard part is the "least" part of showing that ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) is a least upper bound. I don't see how to prove that. But I think I'll start by proving the easy ones, some of which I have stated at #2386 .