## Stream: maths

### Topic: Formalization of the statement that 0.999... = 1

#### Donald Sebastian Leung (Feb 24 2020 at 09:58):

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 (Feb 24 2020 at 10:21):

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

#### Mario Carneiro (Feb 24 2020 at 10:22):

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

#### Johan Commelin (Feb 24 2020 at 10:23):

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 (Feb 24 2020 at 10:23):

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 (Feb 24 2020 at 10:26):

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


Thank you!

#### Mario Carneiro (Feb 24 2020 at 10:28):

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 (Feb 24 2020 at 10:29):

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

#### Mario Carneiro (Feb 24 2020 at 10:29):

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

#### Donald Sebastian Leung (Feb 24 2020 at 10:30):

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

#### Mario Carneiro (Feb 24 2020 at 10:30):

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 (Feb 24 2020 at 10:31):

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

#### Mario Carneiro (Feb 24 2020 at 10:32):

(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 (Feb 24 2020 at 10:36):

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 (Feb 24 2020 at 10:38):

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 (Feb 24 2020 at 10:38):

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 (Feb 24 2020 at 10:39):

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 (Feb 24 2020 at 10:40):

which might mean reorganizing files

#### Donald Sebastian Leung (Feb 24 2020 at 10:40):

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 (Feb 24 2020 at 10:41):

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 (Feb 24 2020 at 10:41):

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 (Feb 24 2020 at 10:41):

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

#### Donald Sebastian Leung (Feb 24 2020 at 10:42):

Mario Carneiro said:

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

Noted

#### Mario Carneiro (Feb 24 2020 at 10:43):

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 (Feb 24 2020 at 10:44):

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 (Feb 24 2020 at 10:48):

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?

yes

#### Donald Sebastian Leung (Feb 24 2020 at 10:48):

Thanks for your feedback and guidance!

#### Mario Carneiro (Feb 24 2020 at 10:50):

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 (Feb 24 2020 at 10:52):

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 (Feb 26 2020 at 17:30):

BTW, SUBMISSION easily follows from has_sum_geometric and has_sum_mul_left.

Last updated: May 11 2021 at 17:39 UTC