## Stream: maths

### Topic: idiomatic statement of sandwich thm

#### Kevin Buzzard (Sep 21 2019 at 16:05):

I occasionally mention the Lean Sandwich theorem all nicely done with @Patrick Massot 's formaliser, but over on #Lean for teaching I was thinking about a bigger real number project and when thinking about limits I realised that we'd just rolled our own with a local is_limit defined as

definition is_limit (a : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, | a n - l | < ε


and developed the theory a way a mathematician would. The students and I were creating proofs of the form

lemma tendsto_iff_sub_tendsto_zero {a : ℕ → ℝ} {l : ℝ} :
is_limit (λ n, a n - l) 0 ↔ is_limit a l :=
begin
split ;
{ intros h ε εpos,
rcases h ε εpos with ⟨N, H⟩,
use N,
intros n hn,
simpa using H n hn }
end


But is there some idiomatic way to do this? What's the idiomatic Lean way to say $a_n\to\ell$?

#### Johan Commelin (Sep 21 2019 at 18:06):

Shouldn't you be using filters instead?

#### Chris Hughes (Sep 21 2019 at 18:11):

tendsto a at_top (nhds l)

#### Patrick Massot (Sep 21 2019 at 19:17):

A few days ago I ran into https://github.com/leanprover-community/mathlib/blob/master/src/analysis/normed_space/basic.lean#L18 and laughed out loud. This was me trying to hide filters. It's a tribute to Mario and Johannes' patience that this line is actually in mathlib.

#### Patrick Massot (Sep 21 2019 at 19:18):

The sandwich theorem itself is at https://github.com/leanprover-community/mathlib/blob/fe1575a0362362d8a49ddb28be2325f1bc526c31/src/topology/algebra/ordered.lean#L227

#### Sebastien Gouezel (Sep 21 2019 at 19:27):

In the sandwich theorem, look at how Lean is not disoriented by the different meanings of b in hgf : {b | g b ≤ f b} ∈ b. That's something that would never pass in a math paper, I guess.

#### Patrick Massot (Sep 21 2019 at 19:32):

Yes, there are a couple of bad jokes like this in mathlib

#### Patrick Massot (Sep 21 2019 at 19:32):

A variation appears in the extension by continuity theorem. I've meant to fix those for ages, but never find enough motivation.

#### Kevin Buzzard (Sep 21 2019 at 22:51):

tendsto a at_top (nhds l)

That's never going to fly with mathematicians. We at least need notation. I guess that's what Patrick is doing. How close can Lean 3 notation get to $\lim_{n\to\infty}a_n=\ell$?

#### Patrick Massot (Sep 22 2019 at 18:25):

My notation was doing exactly that, but trying to mimic $a_n \xrightarrow[n \to \infty]{} l$.

#### Patrick Massot (Sep 22 2019 at 18:30):

Except if was for limits of functions at a point. You can see the result in https://github.com/leanprover-community/mathlib/blob/master/src/analysis/normed_space/basic.lean#L212. The problem with the notation $\lim_{n\to\infty} a_n = l$ is that it overloads the equality symbol, which makes computer scientists nervous.

#### Kevin Buzzard (Sep 22 2019 at 20:59):

Surely "indicates to them that mathematicians use it differently"?

#### Mario Carneiro (Sep 22 2019 at 22:10):

Of course, it's a general communication mechanism, it's not meant to refer to anything in particular. But that sort of thing doesn't fly in a theorem prover

#### Mario Carneiro (Sep 22 2019 at 22:19):

I definitely agree with Ganesalingam that mathematical symbols should be interpreted as another kind of natural language, so that it is not a surprise that a given symbol does not have a single unambiguous context-independent meaning. This is the main difference between computer languages and natural languages of all kinds. But I don't think that it's a deficiency of computer languages, because it forces us to be more precise and prevents communication mistakes

#### Alex J. Best (Sep 22 2019 at 22:45):

Except if was for limits of functions at a point. You can see the result in https://github.com/leanprover-community/mathlib/blob/master/src/analysis/normed_space/basic.lean#L212. The problem with the notation $\lim_{n\to\infty} a_n = l$ is that it overloads the equality symbol, which makes computer scientists nervous.

If $\lim_{n\to\infty}$ was defined to be a partial function on sequences of reals (either to option \R or option ereal with none being limit does not exist) then this wouldn't be an overload right?

#### Simon Hudon (Sep 22 2019 at 22:48):

it is not a surprise that a given symbol does not have a single unambiguous context-independent meaning

We can see that happening already with the + and * symbols. But with = it seems rare to me that the universal = is not a useful notion. Making it context dependent seems kind of risky. But then again, with higher inductive types, you have a bit of that.

#### Simon Hudon (Sep 22 2019 at 22:48):

If $\lim_{n\to\infty}$ was defined to be a partial function on sequences of reals (either to option \R or option ereal with none being limit does not exist) then this wouldn't be an overload right?

That's right

#### Mario Carneiro (Sep 23 2019 at 02:52):

But with = it seems rare to me that the universal = is not a useful notion. Making it context dependent seems kind of risky. But then again, with higher inductive types, you have a bit of that.

To be clear, I am in no way advocating changing the meaning of = in lean; rather I am highlighting that = in math means something else, and we cannot and should not attempt to make lean's = match this notion strictly, because there is not actually a strict definition of = in math if you get down to it. But it is most commonly best approximated by what lean currently calls =, and in other concrete cases we have other definitions like equiv, iso, is_limit, etc for more specialized meanings.

#### Kevin Buzzard (Sep 23 2019 at 06:57):

It is a subtle beast isn't it, the mathematician's equality. If $a_n\in\mathbb{R}$ is a sequence then I am completely happy for $\lim_{n\to\infty}a_n$ to take any of the following values: a set of real numbers (before I've proved that the limit is unique if it exists), a real number (if it exists), "undefined" if it doesn't exist but I haven't talked about tending to infinity yet, and then $+\infty$ and $-\infty$ once these are defined. So I want to be completely flexible about whether this so-called term has type which is a field, a complete bounded totally ordered set (or whatever $[-\infty,+\infty]$ is), or just a genuine option real where it either converges or it doesn't.

#### Kevin Buzzard (Sep 23 2019 at 06:58):

The more I think about it, the more a predicate seems natural. How does one say is_limit (a : nat -> real) -> real -> Prop) idiomatically in Lean?

#### Mario Carneiro (Sep 23 2019 at 07:12):

As chris said, this is tendsto a at_top (nhds l), but you can define is_limit a l to mean this if it suits you

#### Mario Carneiro (Sep 23 2019 at 07:14):

I know you think this looks ridiculous, but it's the most uniform way to handle all those disparate things you just said that you group under the name "limit of a sequence"

#### Mario Carneiro (Sep 23 2019 at 07:15):

all the other encodings, using option real or option ereal or a set of reals or something are more ad hoc and less general

#### Johan Commelin (Sep 23 2019 at 07:16):

You could probably do something like

abbreviation sequence (X : Type*) := ℕ → X

def sequence.tends_to {X : Type*} [topological_space X] (a : sequence X) (x : X) : Prop := tendsto a at_top (nhds x)

example (a : sequence ℝ) : a.tends_to π


#### Johan Commelin (Sep 23 2019 at 07:16):

But it does read nice, I think

#### Johan Commelin (Sep 23 2019 at 07:17):

@Kevin Buzzard I agree with Mario. The best thing is to just teach UGs about filters

#### Mario Carneiro (Sep 23 2019 at 07:20):

if you want to avoid talking about filters, you might try using is_limit defined like this, prove the elementary characterization for metric spaces or explicitly for real sequences, use that equivalence exclusively in proofs, and leave the investigation of the actual definition and the mathlib proofs about limits as advanced material / exercise for the reader

#### Kevin Buzzard (Sep 23 2019 at 07:52):

Kevin Buzzard I agree with Mario. The best thing is to just teach UGs about filters

I supervised a pretty cool 2nd year project on filters last term. No Lean involved, but it was very interesting all the same. They had already done a 2nd year topology course though, so the applications were rather more immediate (quick proof of Tychonoff etc)

Last updated: May 18 2021 at 08:14 UTC