computable min (real)

Stream: general

[Kenny Lau]

Do we have a computable function that gives the minimum of two real numbers?

[Chris Hughes]

I don't think so. Why not write one?

[Andrew Ashworth]

the way reals are defined, how could you decide if any two arbitrary reals are smaller than another

[Andrew Ashworth]

two cauchy sequences could differ only in the eleventy billionth term

[Chris Hughes]

I'm pretty sure it's not possible. Although if reals were implemented differently it might be, so long as they weren't equal.

[Kevin Buzzard]

If the reals were given as actual Cauchy sequences (as some are I guess) then you could just take the min of the Cauchy sequences I guess. But if you just had the equivalence class then what can you do?

[Andrew Ashworth]

turns out i am mistaken, btw, earlier i mentioned it being hard to compute with cauchy sequences

[Andrew Ashworth]

actually i'm watching a presentation on how somebody did exactly that

[Andrew Ashworth]

http://videolectures.net/aug09_spitters_oconnor_cvia/

[Andrew Ashworth]

unfortunately it looks like producing that library was enough work that it was somebody's PhD dissertation

[Andrew Ashworth]

Bishop would be proud

[Chris Hughes]

@Kevin Buzzard quotients are computed as the objects they were quotiented from, so lean has access to the actual cauchy sequences. But how do you find the min of two cauchy sequences in general?

[Kevin Buzzard]

If you have two real numbers represented as Cauchy sequences of rationals then you can just take the termwise min and this will be Cauchy and tend to the min (this is a good exercise ;-) ) ; equality is decidable on the rationals so this shouldn't be a problem I guess. Or am I missing something?

[Chris Hughes]

No, I didn't think of that.

[Kenny Lau]

that's actually exactly the point of this thread. Real inequality is undecidable, but the min function is computable.

[Mario Carneiro]

As Kevin says, given two cauchy sequences and a continuous function of two reals (extending a function on rat) that you want to compute, you can get a cauchy sequence by applying the function pointwise. At no point do you need to decide inequality

[Kenny Lau]

is it easy to do in Lean?

[Mario Carneiro]

Sure, you would just need to show that min is uniformly continuous, which isn't so hard (i.e. |min x y - min z w| <= |x - z| + |y - w|)

[Kenny Lau]

which theorem should I use, after showing that it is uniformly continuous?

[Chris Hughes]

def rmin : cau_seq ℚ abs → cau_seq ℚ abs → cau_seq ℚ abs := λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨λ n, min (x n) (y n), λ ε ε0, begin end⟩

[Chris Hughes]

and then lift to R

[Kenny Lau]

and then one would have to prove that the lift is well-defined

[Mario Carneiro]

That will be the major part of showing that the sequence min (f n) (g n) is cauchy. Then you have to prove that when two cauchy sequences are near their output is also near, so that this lifts to a function on reals. Finally, you prove that it is in fact the min: it is clearly le than reals x and y, and if z <= x and z <= y then z <= min x y.

[Kenny Lau]

right