Zulip Chat Archive

Stream: new members

Topic: Using mathlib for simple concepts


view this post on Zulip Thomas Powell (Feb 03 2021 at 18:59):

I have a naive question about how mathlib is intended to be used. Clicking on a basic concept like convergence on the undergraduate maths page brings me to a very general formulation of convergence in terms of filters, and I'm guessing that many basic facts about convergence are only formalised at this level of abstraction, which of course makes perfect sense.

However, suppose that I'm formalising something which deals with a specific kind of convergence e.g. sequences of real numbers. I want to express this using the straightforward epsilon/delta formulation, but at the same time I want to potentially appeal to basic theorems about convergence which are already proven in mathlib. Is the intended approach that I write out the simple definition and then demonstrate somehow that it is an instance of the abstract concept?

view this post on Zulip Mario Carneiro (Feb 03 2021 at 19:03):

The intended approach is that there is a theorem saying that the general convergence notion in the specific instance is equivalent to the desired characterization

view this post on Zulip Kevin Buzzard (Feb 03 2021 at 19:03):

By this time tomorrow you'll be able to see (in a week_3 directory here) how to prove some basic facts about limits of sequences, and then two-line proofs using filters. The dictionary is there already. For example I define

/-- `l` is the limit of the sequence `a` of reals -/
definition is_limit (a :   ) (l : ) : Prop :=
 ε > 0,  N,  n  N, | a n - l | < ε

but then later on I use

lemma is_limit_iff_tendsto (a :   ) (l : ) :
  is_limit a l  tendsto a at_top (𝓝 l) :=
begin
  rw metric.tendsto_at_top,
  congr',
end

which is already in mathlib. Then e.g. the 20 line proof of "product of limits = limit of products" becomes

example (a b :   ) (l m : ) : is_limit a l  is_limit b m  is_limit (a * b) (l * m) :=
begin
  repeat {rw is_limit_iff_tendsto},
  exact tendsto.mul,
end

view this post on Zulip Mario Carneiro (Feb 03 2021 at 19:04):

For example docs#metric.tendsto_nhds_nhds

view this post on Zulip Bryan Gin-ge Chen (Feb 03 2021 at 19:05):

(We should have this dictionary in an easy-to-find place; maybe some more module docs?)

view this post on Zulip Kevin Buzzard (Feb 03 2021 at 19:06):

Yeah, I couldn't find metric.tendsto_at_top when I was preparing this lecture, I asked in #Is there code for X? and Reid told me about it.

view this post on Zulip Thomas Powell (Feb 03 2021 at 20:27):

Thanks all for the helpful insights, that answers my question perfectly. It's interesting to see how a key part of the game here is constructing the right dictionaries to relevant parts of mathlib


Last updated: May 14 2021 at 23:14 UTC