Thanks and nice! > After inspection, it looks closer to Hales's solution. For formalization, the other solution looks simpler since it does not use induction. The least upper bound is defined in set.mm.
I have stumbled upon the supremum definition but it looks more intricate to use than a manually defining it inline on the real line (unless you’re referring to another definition of the least upper bound). That’s precisely one of the open questions I have about how to go about formalizing this type of proofs! -stan On Thu, Feb 27, 2020 at 7:27 PM Benoit <[email protected]> wrote: > Another proof I just found (sorry, it's not about the formalization): > Let x be such that f(x) \neq 0 and let y \in \R. Set a = g(y). > Set u_n = f(x + ny) for n \in \Z. It satisfies the linear recurrence > relation u_{n+2} = 2a u_{n+1} - u_n. The characteristic relation is r^2 - > 2ar + 1 = 0. The reduced discriminant is D = a^2 - 1. The sequence u_n is > bounded only if D \leq 0, that is, |a| \leq 1 (recall that f(x) \neq 0 and > the sequence is on \Z). > > After inspection, it looks closer to Hales's solution. For formalization, > the other solution looks simpler since it does not use induction. The > least upper bound is defined in set.mm. > > Benoît > > On Thursday, February 27, 2020 at 6:08:41 PM UTC+1, Stanislas Polu wrote: >> >> Hi all, >> >> I'm quite a beginner with Metamath (I have read a bunch of proofs, most >> of the metamath book, I have implemented my own verifier, but I haven't >> constructed any original proof yet) and I am looking to formalize the >> following proof: >> >> IMO B2 1972: http://www.cs.ru.nl/~freek/demos/exercise/exercise.pdf >> Alternative version: >> http://www.cs.ru.nl/~freek/demos/exercise/exercise2.pdf >> >> (More broadly, I think this would be an interesting formalization to have >> in set.mm given this old but nonetheless interesting page: >> http://www.cs.ru.nl/~freek/demos/index.html) >> >> I am reaching out to the community to get direction on how should I go >> about creating an efficient curriculum for myself in order to achieve that >> goal? Any other advice is obviously welcome! >> >> Thank you! >> >> -stan >> > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/27635ef7-bd62-4317-a0f2-9f0873e7c499%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/27635ef7-bd62-4317-a0f2-9f0873e7c499%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0zc9PqLm229NJc2oKxzv%3DpmWZX%2BW1bteJHg%3D5_kSsaQYw%40mail.gmail.com.
