Formalization of the statement that 0.999... = 1

Stream: maths

[Donald Sebastian Leung]

So, after spending about two hours browsing through the standard library for the definition of a limit (among other things) and wrapping my head around the fact that limits are defined from a somewhat more general concept of filters (which I have no idea of as a CS major), I finally got down the following statement (named SUBMISSION in the code example below) which I believe should be logically equivalent to 0.999... = 1:

/- Preloaded.lean -/
import data.rat.basic algebra.geom_sum order.filter.basic topology.basic analysis.specific_limits

open filter

notation `𝓝` := nhds

-- 0.999... = 1
-- Or, more formally:
-- \lim_{n\to+\infty} \frac{9}{10} \sum_{i = 0}^{n - 1} (\frac{1}{10})^i = 1
def SUBMISSION :=
  tendsto (λ n, 9 * geom_series (rat.mk 1 10) n / 10) at_top (𝓝 1)
-- Cheat prevention
notation `SUBMISSION` := SUBMISSION

I would like to ask for feedback on possible improvements (or corrections) to my formalization above. In particular:

• Are there any redundant imports that my statement (SUBMISSION) does not depend on? Ideally, I would like to import as few libraries from mathlib as possible, importing just enough for the statement to compile
• Is there any way I can speed up the compilation time of my file, most of which (I think) is currently spent on importing stuff? I timed lean Preloaded.lean with a stopwatch and it took about 14s to compile and I would like to get it down to well under 12 seconds (the faster the better)
• I noticed in analysis/specific_limits.lean from mathlib that 𝓝 is notation for filter.nhds but I can't seem to use it myself. I also noticed that this was declared as local notation for topological_space (whatever that means). In the meantime, my workaround was to (re-)declare this notation myself to use it in my statement. Is there a way to avoid this workaround, or would you recommend that I just type nhds explicitly in my statement?
• My formalization of the statement 0.999... = 1 seems rather clumsy to me - is there any way I could state it more cleanly (whatever that may mean)?

[Johan Commelin]

@Donald Sebastian Leung Just to comfort you: mathematicians also don't know what a filter is :rolling_on_the_floor_laughing:

[Mario Carneiro]

I think you can use an infinite sum directly rather than a limit of a finite sum

[Johan Commelin]

local notation means that the notation is local to that file, so you would have to repeat that local notation in your file.

[Donald Sebastian Leung]

Mario Carneiro said:

I think you can use an infinite sum directly rather than a limit of a finite sum

Nice. How so?

[Mario Carneiro]

import topology.algebra.infinite_sum

open filter

-- 0.999... = 1
-- Or, more formally:
-- \lim_{n\to+\infty} \frac{9}{10} \sum_{i = 0}^{n - 1} (\frac{1}{10})^i = 1
def SUBMISSION := has_sum (λ i:ℕ, 9 / 10 * (1 / 10) ^ i) 1
-- Cheat prevention
notation `SUBMISSION` := SUBMISSION

[Donald Sebastian Leung]

Thank you!

[Mario Carneiro]

You could also use (∑ i:ℕ, 9 / 10 * (1 / 10) ^ i) = 1 which looks nicer but doesn't exactly assert that the sum is convergent (although if it's not convergent you almost certainly wouldn't be able to prove the equality)

[Donald Sebastian Leung]

So is your first example a more faithful rendering of 0.999... = 1, or does it not really matter?

[Mario Carneiro]

oh, well actually it is defined to return 0 on nonconvergent sums, so that is actually provably equivalent in this case

[Donald Sebastian Leung]

Thanks, I think I will go with your second example then.

[Mario Carneiro]

in practice people will almost certainly have to prove the first statement, but there is an easy lemma to go from that to the second statement

[Mario Carneiro]

fwiw the metamath theorem asserting this uses the second form: 0.999...

[Mario Carneiro]

(yes, the name of the theorem is actually 0.999.... Dot is a valid label character and someone had fun with naming here)

[Mario Carneiro]

However, none of this really helps with the total load time. If you want that, you will probably have to define your own version of the definitions

[Mario Carneiro]

Oops, you need to write it as def SUBMISSION := (∑ i:ℕ, (9 / 10 * (1 / 10) ^ i : ℝ)) = 1 or else it will be false

[Donald Sebastian Leung]

Mario Carneiro said:

However, none of this really helps with the total load time. If you want that, you will probably have to define your own version of the definitions

What is the general stance of defining stuff yourself that is already in the stdlib/mathlib in one form or another, e.g. in order to speed up compilation time?

[Mario Carneiro]

generally frowned upon. It's fine for local work, but if you want to feed back into mathlib you should instead see if you can restructure things to make the definitions have less dependencies

[Mario Carneiro]

which might mean reorganizing files

[Donald Sebastian Leung]

What if it is intended to be published as an (beginner) exercise on an online platform? Would that be akin to teaching bad practices?

[Mario Carneiro]

For a theorem like this, if you are okay with using rational numbers, you can get the statement in only a few lines, skipping the whole theory of topology

[Donald Sebastian Leung]

Mario Carneiro said:

For a theorem like this, if you are okay with using rational numbers, you can get the statement in only a few lines, skipping the whole theory of topology

It's fine as long as it correctly states (something logically equivalent to) 0.999... = 1

[Mario Carneiro]

For a beginner exercise you absolutely want to use mathlib definitions, because newbies can't write the theory

[Donald Sebastian Leung]

Mario Carneiro said:

For a beginner exercise you absolutely want to use mathlib definitions, because newbies can't write the theory

Noted

[Mario Carneiro]

for example a newbie knows that the sum f + g is the sum of f plus the sum of g, but they are not ready to prove that themselves

[Mario Carneiro]

if you give them an undergraduate level definition of the limit, they can probably work with it but that's a separate exercise

[Donald Sebastian Leung]

Mario Carneiro said:

if you give them an undergraduate level definition of the limit, they can probably work with it but that's a separate exercise

If I intend to post the 0.999... exercise as a way for beginners to practice with the concept of a limit (as taught at the undergraduate level), would it be fine to (re-)define the concept in the exercise instead of using the more general definition from mathlib?

[Mario Carneiro]

yes

[Donald Sebastian Leung]

Thanks for your feedback and guidance!

[Mario Carneiro]

teaching material often uses redefinitions, in particular because it makes it easier to prevent students from accidentally or otherwise reusing lemmas from the library that they are supposed to be proving, but this stuff generally doesn't feed back to mathlib

[Donald Sebastian Leung]

Got it. So basically:

• For teaching elementary concepts, redefining stuff already in mathlib is acceptable (and sometimes encouraged)
• For the development of mathlib itself, definitely use as many existing definitions as possible

[Yury G. Kudryashov]

BTW, SUBMISSION easily follows from has_sum_geometric and has_sum_mul_left.