Using mathlib for simple concepts

Stream: new members

[Thomas Powell]

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?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

For example docs#metric.tendsto_nhds_nhds

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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.

[Thomas Powell]

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