Help proving lim_{x->inf} 1/x = 0

Stream: Is there code for X?

[Jonathan Crall]

I'm learning how to use lean4 and to get started I wanted to try and prove that lim_{x->inf} 1/x = 0 (this is actually just a piece of what I'm trying to prove, but it is that I'm having most trouble with). I've found that Mathlib.Order.Filter.Tendsto is probably what I want to encode the notion of a limit, but I was having trouble using it. I started to attempt to prove something simpler: lim_{x -> 2} x * 3 = 6, but I'm not quite sure how to go about it. Seeing an example might help me understand better. (Also is there a way to directly use the epsilon-delta definition of a limit instead of Tendsto, or are they fundamentally the same?)

If it simplifies things, I'm quite happy working in the Rational numbers instead of the Reals. In fact, even if I have a proof for the Reals, I'd like to additionally prove the special case for Rationals - especially if it leads to simplifications of the proof.

If this is not the best place to ask questions like these please direct me to a better forum for my question.

[Mario Carneiro]

Could you show a minimal example of the code you have? #mwe

[Mario Carneiro]

Using the rationals instead of the reals will most likely make your job harder, not easier, because the reals are complete but the rationals aren't

[Mario Carneiro]

but I guess if you want to prove a specific limit and not just an existence claim then it's probably about the same

[Mario Carneiro]

(note: there is no file called Mathlib.Order.Filter.Tendsto, this confused me slightly about your post. The file is called Mathlib.Order.Filter.Basic and it defines a notion called Filter.Tendsto)

[Mario Carneiro]

I am surprised that

import Mathlib

open Filter
example : Tendsto (fun x => 1/x) atTop (nhds (0:ℝ)) := by exact?

turns up empty, and apply?doesn't seem to have anything relevant. I'm sure this is already in the library

[Mario Carneiro]

on the other hand

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

does work, and suggests docs#tendsto_inv_atTop_zero

[Mario Carneiro]

apparently there isn't a similar result about a / x like I would have expected

[Mario Carneiro]

@Jonathan Crall

[Jonathan Crall]

Thank you, this is very helpful. I'm still getting used to the syntax and import system, hence the incorrect usage of terminology. Your correction makes the distinction between files and the symbols they expose more clear (however I'm still a bit confused about how open Filter can work if you just import Mathlib - how does it know about Filter if Filter is defined in Mathlib.Order?)

For a MWE example... working is a very generous description. I figured out enough to make

import Mathlib.Data.Rat.Defs
def reciprocal (x : Rat) : Rat := 1 / x
#eval reciprocal ((10 + 1))

work

but my limit code that I've tried so far is nonsense:

import Mathlib.Order.Filter.Basic
import Mathlib.Order.Filter.AtTopBot
import Mathlib.Topology.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.PSeries
import Mathlib.Data.Real.Pi.Wallis

#check Rat
#check Filter.Tendsto
#check Filter.atTop

theorem Real.tendsto_sum_pi_div_four :
Filter.Tendsto (fun k => Finset.sum (Finset.range k) fun i => (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))

#eval Filter.Tendsto (λ x : Rat => 2 * x) (3) (6)

#check nhds
#check Real.Pi

I was just trying to get a grasp on the concepts. I'm a computer scientist by trade, topology and pure maths is very new to me.

Attempting your code, I had to add in a few imports, but I'm still getting errors:

import «Myfirstproof»
import Mathlib.Order.Filter.Basic
import Mathlib.Topology.Basic
import Mathlib.Data.Real.Basic

open Filter

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

I get:

Main.lean:8:40
failed to synthesize instance
  TopologicalSpace ℝ
Main.lean:8:58
`exact?` could not close the goal. Try `apply?` to see partial suggestions.

It seems upset about (nhds (0:ℝ) and exact?

(Note this is in a vscode environment and I created the project with

elan default stable
elan run --install stable lake new myfirstproof
cd /home/joncrall/code/paper-g1-and-mcc/myfirstproof
lake update
lake exe cache get
lake build

I think I also did some manual modifications to add

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

to lakefile.lean in the myfirstproof directory.

[Mario Carneiro]

import Mathlib means import everything

[Mario Carneiro]

imports are transitive

[Mario Carneiro]

and Mathlib.lean imports every file

[Mario Carneiro]

By importing only Mathlib.Order.Filter.Basic, Mathlib.Topology.Basic and Mathlib.Data.Real.Basic you have imported enough to make sense of the statement but not the proof. The theorem suggested by exact?, tendsto_inv_atTop_zero, lives in Mathlib.Topology.Algebra.Order.Field which is a more advanced file that imports all three of the above files and then adds some more stuff. import Mathlib is just importing the whole library so everything is in there somewhere

[Mario Carneiro]

(Actually you haven't imported enough to make sense of the statement, you need to import whatever provides the instance of TopologicalSpace ℝ. That is, you can't use "the real numbers" and "limits" in the same sentence until you know that the reals are a topological space, and the basic file defining the real numbers doesn't do that)

[Jonathan Crall]

Mario Carneiro said:

imports are transitive

Toto, I have a feeling we're not in coding in Python anymore.

When I run your code verbatim:

import Mathlib
open Filter
example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

It takes a ton of CPU and time and then ultimately returns:

`/home/joncrall/.elan/toolchains/stable/bin/lake print-paths Init Mathlib` failed:

stderr:
info: [1440/1492] Building Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
info: [1498/1562] Building Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
info: [1667/1701] Building Mathlib.Algebra.Homology.Homotopy
info: [1668/1709] Building Mathlib.Algebra.Homology.Opposite
info: [1773/1819] Building Mathlib.Algebra.Module.PID
info: [2004/2085] Building Mathlib.Analysis.NormedSpace.PiLp
info: [2092/2183] Building Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
info: [2111/2201] Building Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
info: [2138/2247] Building Mathlib.FieldTheory.IsAlgClosed.Basic
info: [2424/2711] Building Mathlib.Geometry.Manifold.ContMDiff
info: [2750/3000] Building Mathlib.Computability.TMToPartrec
info: [2963/3242] Building Mathlib.FieldTheory.PerfectClosure
info: [3143/3784] Building Mathlib.RingTheory.RootsOfUnity.Minpoly
info: [3172/3787] Building Mathlib.RingTheory.IsAdjoinRoot
info: [3324/3787] Building Mathlib.RingTheory.Perfection
info: [3376/3787] Building Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
info: [3394/3787] Building Mathlib.RepresentationTheory.Action
info: [3415/3787] Building Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
info: [3421/3787] Building Mathlib.Probability.Notation
info: [3441/3787] Building Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
info: [3442/3787] Building Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
info: [3452/3787] Building Mathlib.Probability.Kernel.CondDistrib
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib:/home/joncrall/.elan/toolchains/stable/lib/lean:/home/joncrall/.elan/toolchains/stable/lib:./lake-packages/mathlib/build/lib /home/joncrall/.elan/toolchains/stable/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./lake-packages/mathlib/././Mathlib/Analysis/NormedSpace/PiLp.lean -R ./lake-packages/mathlib/./. -o ./lake-packages/mathlib/build/lib/Mathlib/Analysis/NormedSpace/PiLp.olean -i ./lake-packages/mathlib/build/lib/Mathlib/Analysis/NormedSpace/PiLp.ilean -c ./lake-packages/mathlib/build/ir/Mathlib/Analysis/NormedSpace/PiLp.c
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5

# Lots more text here

info: [3645/3787] Building Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
info: [3648/3787] Building Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib:/home/joncrall/.elan/toolchains/stable/lib/lean:/home/joncrall/.elan/toolchains/stable/lib:./lake-packages/mathlib/build/lib /home/joncrall/.elan/toolchains/stable/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./lake-packages/mathlib/././Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean -R ./lake-packages/mathlib/./. -o ./lake-packages/mathlib/build/lib/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.olean -i ./lake-packages/mathlib/build/lib/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.ilean -c ./lake-packages/mathlib/build/ir/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.c
error: stdout:
./lake-packages/mathlib/././Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean:225:8: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  (IsOpenMap.functor _).obj ⊤
case h'
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
X Y : Scheme
f : X ⟶ Y
U : ↑(Scheme.affineOpens Y)
H :
  ∀ (U_1 : ↑(Scheme.affineOpens (Scheme.restrict X _))),
    P
      (f.val.c.app (op ↑U) ≫
        X.presheaf.map (eqToHom _).op ≫ (Scheme.ofRestrict (Scheme.restrict X _) _).val.c.app (op ⊤))
V : ↑(Scheme.affineOpens X)
e : ↑V ≤ (Opens.map f.val.base).obj ↑U
U' : Opens ↑↑X.toPresheafedSpace := (Opens.map f.val.base).obj ↑U
e' : (IsOpenMap.functor _).obj ((Opens.map (Opens.inclusion U')).obj ↑V) = ↑V
⊢ (Opens.map (Scheme.ofRestrict X _).val.base).obj ↑V ∈ Scheme.affineOpens (Scheme.restrict X _)
error: external command `/home/joncrall/.elan/toolchains/stable/bin/lean` exited with code 1

./lake-packages/mathlib/././Mathlib/Analysis/NormedSpace/PiLp.lean:422:31: error: Declaration PiLp.aux_uniformity_eq not found.
...

[Mario Carneiro]

oh dear, this is one of the things that you have to learn which is mathlib specific

[Mario Carneiro]

use lake exe cache get to download precompiled mathlib

[Mario Carneiro]

(you should have mentioned that it was building before waiting an hour, this would have saved you the effort!)

[Mario Carneiro]

the errors are not expected though, my guess is that your lean-toolchain doesn't match mathlib, which can cause compile failures

[Mario Carneiro]

use cp lake-packages/mathlib/lean-toolchain lean-toolchain to fix this

[Mario Carneiro]

if it works, lake build should take a few seconds to run, not an hour

[Patrick Massot]

@Jonathan Crall, from this and https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Links.20to.20Resources.20for.20Help, I think you took a wrong start in your Lean adventures. If you are interested in Lean for mathematics you should start learning it using a math-oriented resource. If you go to #mil you will find links to installation instructions that work for maths as well as explanation about limits.

[Kevin Buzzard]

I agree with Patrick. The theorem that 1/n tends to 0 needs all sorts of things like facts about how division plays with inequalities, that natural numbers are nonnegative, that for every real number there's a natural number bigger than it and so on. You can of course battle your way through this if you know how to find your way around the library, but it's not the best exercise for a complete beginner (it looks much easier than it is, from a formal perspective). A much better exercise is to prove that the sum of the limits is the limit of the sums; this is what I do in lecture 2 of my undergraduate lean course and even this has some content. I won't recommend my course to you because it's not yet been translated into lean 4 but like Patrick I will recommend #mil .

[Jonathan Crall]

@Mario Carneiro Following your instructions worked. It took about a minute, but it got there. Many thanks.

My interest in using lean is to provide a formal proof for a relationship I found between the MCC and FM measures of a confusion matrix namely the FM is the limit of the MCC as the true negative count tends to infinity. I've written it up here: https://arxiv.org/abs/2305.00594 and I'm fairly sure the informal proof is correct, I've also verified it with sympy, but that only goes so far. Prooving lim_{x -> inf} 1/x = 0 is the main step.

Mathematics in Lean (MIL) looks very helpful. Thank you for the pointer.

EDIT: I forgot the proof also includes a square root operation, so proving it in the rationals wont be possible without modification (or maybe if I restrict to algebreic numbers that would be easier?).

[Ming Li]

With the code and the idea about the real line, how to find the related data from Mathlib? or how to modify the code so that lean can give useful suggestion? "unexpected token 'fun'; expected '_' or identifier" is given here.

Mario Carneiro said:

on the other hand

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

does work, and suggests docs#tendsto_inv_atTop_zero

[Alex J. Best]

What is the whole file that gives you that error message?
If I do

import Mathlib

open Filter

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

I don't see any issues

[Ming Li]

Thanks. I fixed the issue caused by /--/.
Alex J. Best said:

What is the whole file that gives you that error message?
If I do

import Mathlib

open Filter

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

I don't see any issues

[Ming Li]

Are MIL and Mathlib4 compatible to each other? In general, how to merge two libraries?

Patrick Massot said:

Jonathan Crall, from this and https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Links.20to.20Resources.20for.20Help, I think you took a wrong start in your Lean adventures. If you are interested in Lean for mathematics you should start learning it using a math-oriented resource. If you go to #mil you will find links to installation instructions that work for maths as well as explanation about limits.

[Ruben Van de Velde]

MIL depends on mathlib: https://github.com/leanprover-community/mathematics_in_lean

Not sure what you mean by "merge" in this context

[Ming Li]

Thanks for reply. By "merge", I mean that suppose there is another tototial like MIL, also depending on mathlib4 and lean4, how can I use both in a single *.lean file?

Ruben Van de Velde said:

MIL depends on mathlib: https://github.com/leanprover-community/mathematics_in_lean

Not sure what you mean by "merge" in this context

[Ruben Van de Velde]

Yes, you can do that. You should make sure that the versions match up, though

[Ming Li]

Simply moving library folder dose not work. Any suggestion?

[Alex Altair]

@Mario Carneiro @Jonathan Crall I'm just jumping into the middle of this, but surely one doesn't need to involve topology for the limit of 1/x? From browsing the docs, I see this lemma, which seems like the same thing but without topology

[Mario Carneiro]

@Alex Altair The definition of tendsto doesn't involve topology, but usually the next step will. atTop needs an ordering on the type, and nhds is a topological filter

[Mario Carneiro]

so that statement does involve topology

[Jireh Loreaux]

I'm curious why you think "surely one doesn't need to involve topology for the limit of 1/x?" Or why you think docs#IsROrC.tendsto_inverse_atTop_nhds_0_nat didn't use topology.

[Kevin Buzzard]

The definition of tendsto might strictly speaking not involve topology, but it either involves epsilons and deltas or it involves filters, and both of those are topology in disguise (the filter is a topological neighbourhood filter in the application)

[Alex Altair]

I see, that makes sense

[Alex Altair]

@Jireh Loreaux One reason is that limits were understood hundreds of years before people had a concept of topology, and even formalized long before, via the epsilon-delta stuff (in the mid-1800s I think?). We also teach limits before topology, and I don't think calculus classes are sweeping foundations under the rug when they do so without using any language like "open set"

[Alex Altair]

(I didn't realize docs#IsROrC.tendsto_inverse_atTop_nhds_0_nat used topology just because I didn't see the word "topology" anywhere on the page, and I don't have any familiarity with how Mathlib is structured yet)

[Patrick Massot]

I think we need more context to help you. If you are teaching first year undergrads and want to use limits of sequences of real numbers or functions from real numbers to real numbers then clearly you should redefine limits in elementary terms, just like in the tutorial project or in GlimpseOfLean. But if you want to contribute to a full scale math library like mathlib then it makes no sense.

[Jireh Loreaux]

Aha, yes, that makes sense. I think here the point is that the structure of mathlib is relevant. In general, within mathlib, we opt for the most general (modulo convenience and some other considerations) setting possible. So, although limits were originally formulated by Cauchy with ε > 0, ..., that definition doesn't work in more general settings. Instead, convergence (to a point) makes sense in topological spaces. However, because we want to allow even more generality (e.g., aₙ → ∞ as n → ∞), we encapsulate limits in terms of filters, and then convergence to a point x in a topological space is encoded using the neighborhood filter 𝓝 x (i.e., docs#nhds), which is defined in terms of the topology.

For a nice description of why we work in this generality, have a look at Patrick's ICERM talk from last year: https://icerm.brown.edu/video_archive/?play=2899 So, it doesn't have anything to do with wanting to avoid "sweeping foundations under the rug", but rather, with usability, feasibility and convenience.

As Patrick mentioned, this generality isn't suitable for presentation to early undergraduates, so if you are teaching you probably want to roll your own (even if the definitions are connected to Mathlib's docs#Filter.Tendsto behind the curtain).

[Ming Li]

Does it mean that mathlib4 is research oriented while tutorials like GlimpseOfLean is educational one?

[Patrick Massot]

GlimpseOfLean is an introduction to Lean. You can start with it and then learn about the mathlib way in #mil which requires a much larger time investment.

[Ming Li]

Indeed, both are great for beginners. So the particular tactics are designed for educational purpose. They will not be used in Mathlib4, right?

[Gabor Nyeki]

Mario Carneiro said:

on the other hand

example : Tendsto (fun x => x⁻¹) atTop (nhds (0:ℝ)) := by exact?

does work, and suggests docs#tendsto_inv_atTop_zero

When I try this, I get a typeclass error:

import Mathlib

example : Filter.Tendsto (fun (x : ℝ) => x⁻¹) atTop (nhds 0) := by
  refine tendsto_inv_atTop_zero

typeclass instance problem is stuck, it is often due to metavariables
  OrderTopology ?m.721

Why is ℝ not recognized as an instance of OrderTopology?

[Gabor Nyeki]

The error disappears if I also add open Filter.

[Yongyi Chen]

atTop is actually Filter.atTop. Without open Filter, Lean was interpreting it as an implicit variable.

[Anatole Dedecker]

If you want to disable this (it can be very annoying sometimes) you can add set_option autoImplicit false at the beginning of the file