Performing computations when applying a lemma

Stream: Is there code for X?

[Flo (Florent Schaffhauser)]

Hi!

As an exercise (for me), I have formalised the following lemma:

import data.real.basic

def sequence_tendsto (u : ℕ → ℝ) (l : ℝ) :=
∀ ε > 0, ∃ N : ℕ, ∀ n > N, |u n - l| < ε

def continuous_function_at (f : ℝ → ℝ) (x0 : ℝ) :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x0| < δ → |f(x) - f(x0)| < ε

lemma limit_f_circ_u (f : ℝ → ℝ) (u : ℕ → ℝ) (x0 : ℝ) :
(sequence_tendsto u x0) ∧ (continuous_function_at f x0) →
sequence_tendsto (f ∘ u) (f x0) :=

But now I would like to apply it to the following example:

def g ( x : ℝ ) := 1+x

noncomputable def v (n : ℕ) := (1/↑n : ℝ)

example : sequence_tendsto (g∘v) (g 0) :=

I started off like this:

begin
apply limit_f_circ_u g v 0,
split,
show (∀ ε>0, ∃ N : ℕ, ∀ n > N, |v n - 0| < ε),
simp,
assume (ε ε_pos),
let N := nat.floor (1/ε),
use N,
intro n,
intro h,
rw v,
simp,

end

So now my goal is |(↑n)⁻¹| < ε. I have tried a bunch of things and I am getting close but it is all very ugly. Is there an approach that you would recommend to handle such computations when applying a lemma?

If my function g and my sequence v were more complicated, it would be even more tedious to find the correct N and δ and show that v has a limit x0 and that g is continuous at x0, so any suggestion would be greatly appreciated :-)

Here is for instance what I wrote to prove that g is continuous at 0:

show (∀ ε>0, ∃ δ>0, ∀ x : ℝ , |x - 0| < δ → |g x - g 0| < ε),
intros ε ε_pos,
rw g,
simp,
let δ := ε,
use δ,
split,
exact ε_pos,
intro x,
intro x_small,
rw g,
simp,
exact x_small,

All comments are welcome! Thank you :-)

[Johan Commelin]

@Flo (Florent Schaffhauser) Do you know about filters?

[Johan Commelin]

They allow you to work with limits and such without needing to find N and delta etc

[Johan Commelin]

And this is what mathlib does all over the place.

[Johan Commelin]

A very brief explanation can be found at https://leanprover-community.github.io/mathlib_docs/order/filter/basic.html#top

[Johan Commelin]

A somewhat longer explanation is https://leanprover-community.github.io/theories/topology.html

[Flo (Florent Schaffhauser)]

I see. So this type of concrete question should be dealt with using filters?

I know the mathematical object, so I can probably use them here. I will look at the reference and search for examples! Thanks :-)

[Johan Commelin]

Sometimes you need to do a concrete calculation. Then mathlib provides a lemma that puts you back in epsilon-delta world. But for things like: composition of limits, it is very much prefered to work with filters.

[Johan Commelin]

src#filter.tendsto.comp -- the proof is now a 1-liner!

[Flo (Florent Schaffhauser)]

I suppose that in a lecture I would just say "this sequences tends to 0 and this function is continuous at 0 so..." but not prove it in more detail. If asked about the function, I would just say it's a polynomial function, so it's continuous. I'm sure I can find that somewhere in Mathlib. But I am not sure what kind of argument I would use for the sequence if I was asked to provide one (except for going back to the epsilon-delta definition).

[Flo (Florent Schaffhauser)]

I should have mentioned that this is the type of exercise I would like to ask my students to solve in my course next semester, so that's also why I am trying to find a basic approach.

[Johan Commelin]

I think Patrick succesfully teaches filters. They shouldn't be too hard to demystify

[Flo (Florent Schaffhauser)]

Yes, I'll check the webpage for his course again. Thanks for the suggestion :)

[Patrick Massot]

I teach filters to mathematicians, not to my first year undergrads.

[Patrick Massot]

With my first years undergrad I don't do concrete computations, only abstract proofs. They do concrete computations for one full term before coming to my class. My class is all about abstract proofs. I do need that 1/n goes to zero but I give it as a lemma they don't need to prove.

[Flo (Florent Schaffhauser)]

Patrick Massot said:

I do need that 1/n goes to zero but I give it as a lemma they don't need to prove.

OK, I see. Thanks :-)

[Flo (Florent Schaffhauser)]

By the way, if I have

def sequence_tendsto (u : ℕ → ℝ) (l : ℝ) :=
∀ ε > 0, ∃ N : ℕ, ∀ n > N, |u n - l| < ε

noncomputable def v (n : ℕ) := (1/↑n : ℝ)

example : sequence_tendsto (g∘v) (g 0) :=

and in tactic mode I write

show (∀ ε>0, ∃ N : ℕ, ∀ n > N, |v n - 0| < ε),
simp,

is there a way to have Lean understand if I writeshow (∀ ε>0, ∃ N : ℕ, ∀ n > N, |v n| < ε) directly?

[Ruben Van de Velde]

Does simp [sequence_tendsto] work as a proof?

[Johan Commelin]

@Flo (Florent Schaffhauser) Do you mean that you want to write the show statement, and the simp should be done by Lean behind the scenes?

[Flo (Florent Schaffhauser)]

@Johan Commelin I mean either write
show (∀ ε>0, ∃ N : ℕ, ∀ n > N, |v n - 0| < ε)
and have Lean give me directly
∀ (ε : ℝ), 0 < ε → (∃ (N : ℕ), ∀ (n : ℕ), N < n → |v n| < ε)
as a goal (without having to enter simp,). Or, better yet, simply write
show (∀ ε>0, ∃ N : ℕ, ∀ n > N, |v n | < ε)
and have Lean understand that this indeed matches what appears in def sequence_tendsto because here l=0.

[Johan Commelin]

Aha, maybe

suffices : (∀ ε>0, ∃ N : ℕ, ∀ n > N, |v n | < ε),
{ by simpa [sequence_tendsto] },

will work?

[Flo (Florent Schaffhauser)]

Ruben Van de Velde said:

Does simp [sequence_tendsto] work as a proof?

Oh! Yes, it does! Thanks :-))

[Flo (Florent Schaffhauser)]

To sum up: when the goal is

⊢ sequence_tendsto v 0

then entering

simp [sequence_tendsto],

changes the goal to

⊢ ∀ (ε : ℝ), 0 < ε → (∃ (N : ℕ), ∀ (n : ℕ), N < n → |v n| < ε)

which is what I wanted.

[Flo (Florent Schaffhauser)]

Johan Commelin said:

Aha, maybe

suffices : (∀ ε>0, ∃ N : ℕ, ∀ n > N, |v n | < ε),
{ by simpa [sequence_tendsto] },

will work?

Also works! Thank you both :)

[Kevin Buzzard]

@Flo (Florent Schaffhauser) I do limits and continuity the way it's taught to first year undergraduates when I teach my lean course and I never mention filters to them.

[Flo (Florent Schaffhauser)]

Hi @Kevin Buzzard ! Great, I want to do that too.

And would you suggest to use the fact that 1/n tends to zero without proof? Or is it something that you think is worth proving in an introductory course? I will look again at your course more in detail.

I think that I would like to ask my students to prove such facts formally, but my concern is that I may write something unnecessarily complicated because I’m not aware of the correct tactics to use for such things.

[Patrick Massot]

Did you do the tutorials project? It is based on what I was doing with my students three years ago (and what I'm doing currently is not very different except it uses controlled natural languages tactics).

[Flo (Florent Schaffhauser)]

I believe this is where I took the lemma from :sweat_smile: Then I just thought I would add some non-abstract examples. So it is really with the computations that I am running into trouble.

[Kevin Buzzard]

simp,
  -- ⊢ |(↑n)⁻¹| < ε
  -- I wouldn't have defined N, it's just getting in the way
  change ⌊1 / ε⌋₊ < n at h,
  -- know |n⁻¹|=n⁻¹
  rw abs_eq_self.2, -- I guessed the name
  -- x⁻¹ < y ↔ y⁻¹ < x
  rw inv_lt, -- I guessed the name
  -- now work on h; I guessed the name of the lemma
  rw nat.floor_lt at h,
  -- change ε⁻¹ to 1/ε ; I guessed the name
  rw inv_eq_one_div,
  exact h,
  -- now we're done apart from a bunch of non-negativity hypotheses
  all_goals {try {positivity}},
  -- only one failed to die, namely 0 < ↑n; do this manually
  norm_cast,
  refine lt_of_le_of_lt _ h,
  exact zero_le ⌊1 / ε⌋₊, -- I used library_search for this one
  sorry, -- continuity goal remains
end

[Patrick Massot]

Choosing the topics and exercises that will be possible to do with Lean without introducing any artificial difficulty is a very important part of teaching with Lean. Fortunately that still leaves a lot of options. If you want to focus on computations you should probably ask @Heather Macbeth.

[Flo (Florent Schaffhauser)]

Thank you @Kevin Buzzard , now it works! For some reason, positivity is not recognised in my example, so I had to write a bit more.

Next I will try without defining N :sweat_smile:

[Flo (Florent Schaffhauser)]

Patrick Massot said:

If you want to focus on computations you should probably ask Heather Macbeth.

Yes, I will definitely do that! But first I should read more from Algebraic computations in Lean :blush:

[Flo (Florent Schaffhauser)]

Thank you everyone.

[Notification Bot]

Flo (Florent Schaffhauser) has marked this topic as resolved.

[Notification Bot]

Flo (Florent Schaffhauser) has marked this topic as unresolved.

[Flo (Florent Schaffhauser)]

Not quite sure if I should use that check mark... sorry.

[Flo (Florent Schaffhauser)]

Kevin Buzzard said:

-- I wouldn't have defined N, it's just getting in the way

Actually, this is pretty basic stuff but I am not sure how to solve a goal like the following one without defining an N:

ε: ℝ
ε_pos: 0 < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N < n → |1/(↑n)| < ε

I'll think more about it.

[Jireh Loreaux]

Use the archimedean property.

[Jireh Loreaux]

If you want to get almost all the way there: docs#exists_nat_one_div_lt, but if you want to hew closer to the definition of archimedean, you could do more work and start from docs#exists_nat_gt

[Kevin Buzzard]

@Flo (Florent Schaffhauser) I had to import tactic (the thing I tell all my students to start with)

[Jireh Loreaux]

For instance:

import data.real.basic

example (ε : ℝ) (ε_pos: 0 < ε) :
  ∃ (N : ℕ), ∀ (n : ℕ), N < n → |1/(↑n)| < ε :=
begin
  obtain ⟨N, hN⟩ := exists_nat_one_div_lt ε_pos,
  refine ⟨N + 1, λ n hn, _⟩,
  have hN' : 0 < (N + 1 : ℝ) := by exact_mod_cast N.succ_pos,
  have hn' : 0 < (n : ℝ) := hN'.trans (by exact_mod_cast hn),
  calc |1 / (n : ℝ)| = 1 / (n : ℝ)
      : abs_of_nonneg (one_div_nonneg.mpr hn'.le)
  ... < 1 / (N + 1 : ℝ) : (one_div_lt_one_div hn' hN').mpr (by exact_mod_cast hn)
  ... < ε : hN,
end

I'm not saying this is the absolute cleanest way. The nasty bit is of course the coercions, but that's handled with exact_mod_cast everywhere. However, I would generally recommend hiding coercions from students until it really becomes necessary.

[Kevin Buzzard]

And you can just put use thing, instead of let N := thing, use N

[Flo (Florent Schaffhauser)]

And you can just put use thing, instead of let N := thing, use N

Got it. Thanks!

[Flo (Florent Schaffhauser)]

Kevin Buzzard said:

Flo (Florent Schaffhauser) I had to import tactic (the thing I tell all my students to start with)

Huh, funny: this morning I actually added import tactic to my file but still got the following message

unknown identifier 'positivity'

I am working within the mathematics in Lean project.

[Kevin Buzzard]

Oh I don't know what version of mathlib that's on. Probably we should bump it, by the sounds of things

[Patrick Massot]

Yes, it probably runs an old mathlib.

[Flo (Florent Schaffhauser)]

I see. Thanks!