Zulip Chat Archive

Stream: maths

Topic: idiomatic statement of sandwich thm


view this post on Zulip 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 ana_n\to\ell?

view this post on Zulip Johan Commelin (Sep 21 2019 at 18:06):

Shouldn't you be using filters instead?

view this post on Zulip Chris Hughes (Sep 21 2019 at 18:11):

tendsto a at_top (nhds l)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 21 2019 at 19:32):

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

view this post on Zulip 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.

view this post on Zulip 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 limnan=\lim_{n\to\infty}a_n=\ell?

view this post on Zulip Patrick Massot (Sep 22 2019 at 18:25):

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

view this post on Zulip 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 limnan=l\lim_{n\to\infty} a_n = l is that it overloads the equality symbol, which makes computer scientists nervous.

view this post on Zulip Kevin Buzzard (Sep 22 2019 at 20:59):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 limnan=l\lim_{n\to\infty} a_n = l is that it overloads the equality symbol, which makes computer scientists nervous.

If limn\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?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Sep 22 2019 at 22:48):

If limn\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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 06:57):

It is a subtle beast isn't it, the mathematician's equality. If anRa_n\in\mathbb{R} is a sequence then I am completely happy for limnan\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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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 π

view this post on Zulip Johan Commelin (Sep 23 2019 at 07:16):

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

view this post on Zulip Johan Commelin (Sep 23 2019 at 07:16):

But it does read nice, I think

view this post on Zulip Johan Commelin (Sep 23 2019 at 07:17):

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

view this post on Zulip 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

view this post on Zulip 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