idiomatic statement of sandwich thm

Stream: maths

[Kevin Buzzard]

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]

Shouldn't you be using filters instead?

[Chris Hughes]

tendsto a at_top (nhds l)

[Patrick Massot]

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]

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

[Sebastien Gouezel]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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

[Patrick Massot]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

Of course this doesn't help you with undefined limits or infinity

[Johan Commelin]

But it does read nice, I think

[Johan Commelin]

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

[Mario Carneiro]

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]

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)