Zulip Chat Archive

Stream: maths

Topic: Link between sequential and epsilon/delta versions


view this post on Zulip Ryan Lahfa (Apr 03 2020 at 19:04):

In real analysis, we often encounter sequential version of usual epsilon/delta definitions.

For example, sequential continuity, sequential uniform continuity, accumulation point of a set/sequence, inf/sup.

I have multiple questions Lean and non-Lean ones:

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?
(2) It looks like that the equivalence theorem between a sequential version and an epsilon/delta one is also independent of the concept and relies more on the form of the definition rather than on its contents, so, we should be able to produce the equivalence theorem given just a general version of such definitions, right? (under some assumption of choice for sequential → epsilon/delta).
(3) Is this something I could formalize in Lean? Would it be better to go for a type class in such cases?

Maybe, this question is not very relevant because it's impossible to have a general form of sequential version of definitions or things like that.

To give precise examples, here are definitions:

Accumulation point aa of a sequence xx:

Epsilon/Delta: ε>0,n0,Nn,xna<ε\forall \varepsilon > 0, \forall n \geq 0, \exists N \geq n, \lvert x_n - a\rvert < \varepsilon
Sequence form: yx(N)N,limn+yn=a\exists y \in x(\mathbb{N})^{\mathbb{N}}, \lim_{n \to +\infty} y_n = a

Sup:
We say that a=supAa = \sup A if:

Epsilon/Delta: ε>0,xA,aε<xa\forall \varepsilon > 0, \exists x \in A, a - \varepsilon < x \leq a
Sequence form: yAN,limn+yn=a\exists y \in A^{\mathbb{N}}, \lim_{n \to +\infty} y_n = a

Continuity:
We say that f:ABf : A \to B is continuous at xAx \in A if:

Epsilon/delta: ε>0,δ>0,yA,xyδ    f(x)f(y)ε\forall \varepsilon > 0, \exists \delta > 0, \forall y \in A, \lvert x - y \rvert \leq \delta \implies \lvert f(x) - f(y) \rvert \leq \varepsilon
Sequence form: xAN,(limn+xn=x)    (limn+f(xn)=f(x))\forall x \in A^{\mathbb{N}}, \left(\lim_{n \to +\infty} x_n = x\right) \implies \left(\lim_{n \to +\infty} f(x_n) = f(x)\right)

view this post on Zulip Mario Carneiro (Apr 03 2020 at 19:35):

Filters are the unifying abstraction here

view this post on Zulip Mario Carneiro (Apr 03 2020 at 19:37):

In general topological spaces, sequential versions of many concepts exist and are different from the usual ones

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 19:37):

Mario Carneiro said:

Filters are the unifying abstraction here

I wanted to avoid those :D… But I guess this is it

view this post on Zulip Mario Carneiro (Apr 03 2020 at 19:39):

Given a sequence there is a filter defined by "containing cofinitely many of the points of the sequence", and a limit of the filter is the same as a limit of the sequence

view this post on Zulip Mario Carneiro (Apr 03 2020 at 19:42):

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

Actually, the logical manipulation you are doing to the definitions to get this is well known elsewhere as "skolemization", the interchanging of \all x, \exists y, P x y with \ex f, \forall x, P x (f x)

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 19:43):

Mario Carneiro said:

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

Actually, the logical manipulation you are doing to the definitions to get this is well known elsewhere as "skolemization", the interchanging of \all x, \exists y, P x y with \ex f, \forall x, P x (f x)

Okay, I was remembering something in terms of "skolemization" and logic, but could not find what I needed. Thank you so much!

view this post on Zulip Mario Carneiro (Apr 03 2020 at 19:44):

although in order to make them sequences there is an additional step where you weaken the real number epsilon quantifier to an equivalent natural number quantifier

view this post on Zulip Mario Carneiro (Apr 03 2020 at 19:44):

(which is where the difference is in general, non first countable topological spaces)

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 19:46):

Okay, it makes a lot of sense now, thank you!

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 19:54):

Mario Carneiro said:

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

Actually, the logical manipulation you are doing to the definitions to get this is well known elsewhere as "skolemization", the interchanging of \all x, \exists y, P x y with \ex f, \forall x, P x (f x)

BTW, is there any skolemization lemma in Lean?

view this post on Zulip Alex J. Best (Apr 03 2020 at 20:00):

classical.skolem in core lean?

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 20:04):

If you're formalising analysis in tactic mode you might never need to use terms such as this though

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 20:08):

Kevin Buzzard said:

If you're formalising analysis in tactic mode you might never need to use terms such as this though

Why?

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 20:09):

My problem is I often run into those dual definitions when I'm attempting to proof stuff.

And, when let's say I have a proof of having an accumulation point in an epsilon/delta-style, I'm not sure how to convert it into a sequence-style proof easily without writing a lot of machinery (?).

view this post on Zulip Patrick Massot (Apr 03 2020 at 20:21):

You shouldn't be afraid of filters. They are much nicer than epsiloneries.

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 20:24):

Patrick Massot said:

You shouldn't be afraid of filters. They are much nicer than epsiloneries.

All the contrary, I love them; but I am not allowed to use them because of most students (and maybe non-topologists teachers) which do not understand them very well

But at the same time, I'm frustrated with repeating the same boring & technical proofs…

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 20:51):

Ryan Lahfa said:

Kevin Buzzard said:

If you're formalising analysis in tactic mode you might never need to use terms such as this though

Why?

Because we have tactics like choose.

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 20:54):

Kevin Buzzard said:

Ryan Lahfa said:

Kevin Buzzard said:

If you're formalising analysis in tactic mode you might never need to use terms such as this though

Why?

Because we have tactics like choose.

Wow. That's awesome!

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 21:53):

Though, I come back with an MWE because I didn't succeed to make choose work well.

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X  X  )
(d_pos :  x y, d x y  0)
(presep :  x y, x=y  d x y = 0)
(sep :  x y, d x y = 0   x = y)
(sym :  x y, d x y = d y x)
(triangle :  x y z, d x z  d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

def converge (x:   X) (l : X) :=
   ε > 0,  N,  n  N, ((d l (x n))  < ε)

lemma sup_is_a_cv_seq [conditionally_complete_linear_order X] (S: set X):
  S.nonempty  bdd_above S   (x:   X), (set.range x)  S  converge x (Sup S) := begin
  intros hnn hbdd,
  end

Let's say I want to prove that sup_is_a_cv_seq, so ideally, I should be able to reuse some parts of mathlib, namely cSup_intro I imagine and taking ϵ = 1/n for all n ≥ 0, this way, I should be able to have this lemma easily w/o rewriting a lot of stuff, right?

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:09):

Specifically, if I try to do this:

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X  X  )
(d_pos :  x y, d x y  0)
(presep :  x y, x=y  d x y = 0)
(sep :  x y, d x y = 0   x = y)
(sym :  x y, d x y = d y x)
(triangle :  x y z, d x z  d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

def converge (x:   X) (l : X) :=
   ε > 0,  N,  n  N, ((d l (x n))  < ε)

lemma sup_is_a_cv_seq [conditionally_complete_linear_order X] (S: set X):
  S.nonempty  bdd_above S   (x:   X), (set.range x)  S  converge x (Sup S) := begin
  intros hnn hbdd,
  have:  ε > 0,  x  S, d (Sup S) x < ε := sorry,
  have:  (N: ),  x  S, d (Sup S) x < 1/(N + 1) := sorry,

  choose x hrange h using this,
  use x,
  split,
  intros y hy,
  obtain  N, hN  := hy,
  rw  hN,
  exact hrange N,
  intros ε ,
  -- 1/(N + 1) ≤ eps
  -- 1/eps ≤ N + 1
  -- 1/eps - 1 ≤ N
  -- use (floor(1/eps - 1) + 1)
  use (floor((1/ϵ) - 1) + 1),


  end

The use won't work.

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:09):

Because floor is in Z and I have to prove that the total value is in N, I guess.

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:12):

Huh, no, the code provided uses a ϵ and the ε is not the same…

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:16):

Wonder if it is my CPU or something, but:

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X  X  )
(d_pos :  x y, d x y  0)
(presep :  x y, x=y  d x y = 0)
(sep :  x y, d x y = 0   x = y)
(sym :  x y, d x y = d y x)
(triangle :  x y z, d x z  d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

def converge (x:   X) (l : X) :=
   ε > 0,  N,  n  N, ((d l (x n))  < ε)

lemma sup_is_a_cv_seq [conditionally_complete_linear_order X] (S: set X):
  S.nonempty  bdd_above S   (x:   X), (set.range x)  S  converge x (Sup S) := begin
  intros hnn hbdd,
  have:  ε > 0,  x  S, d (Sup S) x < ε := sorry,
  have:  (N: ),  x  S, d (Sup S) x < 1/(N + 1) := sorry,
  choose x hrange h using this,
  use x,
  split,
  intros y hy,
  obtain  N, hN  := hy,
  rw  hN,
  exact hrange N,
  intros ε ,
  -- 1/(N + 1) ≤ eps
  -- 1/eps ≤ N + 1
  -- 1/eps - 1 ≤ N
  -- use (floor(1/eps - 1) + 1)
  set N₀ := (floor((1/ε) - 1) + 1),
  have N0_pos: N₀  0 := sorry,
  -- lift N₀ to ℕ using N0_pos,
  use N₀,

  sorry,
  end

is taking a lot of time to compute.

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:29):

presep could be less clunkily expressed as forall x, d x x = 0, and d_pos follows from triangle and sym and presep

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:30):

Kevin Buzzard said:

presep could be less clunkily expressed as forall x, d x x = 0, and d_pos follows from triangle and sym and presep

Thank you!

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:31):

I am concerned about your first sorry

view this post on Zulip Mario Carneiro (Apr 03 2020 at 22:31):

at the risk of pointing out the obvious, mathlib already has a definition of metric spaces

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:31):

But what about a metric space which is also a conditionally complete linear order?

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:31):

Because I am concerned that these two structures, the way you have set things up, are completely unrelated.

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:32):

Mario Carneiro said:

at the risk of pointing out the obvious, mathlib already has a definition of metric spaces

I know, this is rather to have another metric space definition which does not use filters, but only standard sequences.

view this post on Zulip Mario Carneiro (Apr 03 2020 at 22:32):

but the definition doesn't say anything about sequences

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:32):

For example I don't see any reason why Sup S (which is defined using the complete linear order structure) should have anything to do with converge (which is defined using he metric space)

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:32):

Kevin Buzzard said:

Because I am concerned that these two structures, the way you have set things up, are completely unrelated.

Yes, I definitely feel super wrong about this too. But in order to talk about Sup, I need some structure where bounded above gives me a sup.

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:33):

Sure, but you haven't glued your two choices of structure together

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:33):

Kevin Buzzard said:

For example I don't see any reason why Sup S (which is defined using the complete linear order structure) should have anything to do with converge (which is defined using he metric space)

Wouldn't cSup_intro give me the first sorry?

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:33):

You can't prove any theorem relating sups to distances here

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:33):

Mario Carneiro said:

but the definition doesn't say anything about sequences

Of metric spaces?

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:33):

Kevin Buzzard said:

You can't prove any theorem relating sups to distances here

I see what you mean, right.

view this post on Zulip Mario Carneiro (Apr 03 2020 at 22:34):

I think you want to know that the topology is orderable

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:34):

You have currently written "Let XX be a metric space. Assume also that XX has a total order, which is completely unrelated to the metric space structure. Then..."

view this post on Zulip Mario Carneiro (Apr 03 2020 at 22:34):

but that requires the topology of the metric space, so at that point you are better off using the mathlib definition

view this post on Zulip Mario Carneiro (Apr 03 2020 at 22:35):

You can probably recast it in terms of compatibility directly, something like "intervals contain open balls and vice versa"

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:39):

Let's assume I want to prove this only for R\mathbb{R} right now, so the first sorry is not a problem anymore, right? I can just remove the total orderable condition.

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:41):

Okay, I see now why the first sorry was not feasible, indeed.

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:51):

If you don't want to work with R\mathbb{R} directly you need to come up with some structure where the ideas you want to formalise are still true, and it sounds to me like you want the topology induced by the metric to equal the topology induced by the order.

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:52):

So either you formalise what the topology induced by your metric is, or you use mathlib metric spaces where it's already there.

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:53):

I'll directly work with R\mathbb{R} right now because I won't use this lemma for something else than R\mathbb{R}.
After I succeed, I'll revisit it to improve it with the topology order condition rather.

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:53):

My whole code becomes now:

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X  X  )
(d_pos :  x y, d x y  0)
(presep :  x y, x = y  d x y = 0)
(sep :  x y, d x y = 0   x = y)
(sym :  x y, d x y = d y x)
(triangle :  x y z, d x z  d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

instance real.metric_space : metric_space  :=
{ d                  := λx y, abs (x - y),
  d_pos              := by simp [abs_nonneg],
  presep             := begin simp, apply sub_eq_zero_of_eq end,
  sep                := begin simp, apply eq_of_sub_eq_zero end,
  sym                := assume x y, abs_sub _ _,
  triangle           := assume x y z, abs_sub_le _ _ _ }

theorem real.dist_eq (x y : ) : d x y = abs (x - y) := rfl

theorem real.dist_0_eq_abs (x : ) : d x 0 = abs x :=
by simp [real.dist_eq]

def converge (x:   X) (l : X) :=
   ε > 0,  N,  n  N, ((d l (x n))  < ε)


lemma sup_is_a_cv_seq (S: set ):
  S.nonempty  bdd_above S   (x:   ), (set.range x)  S  converge x (Sup S) := begin
  intros hnn hbdd,
  have:  ε > 0,  x  S, Sup S - x < ε := sorry,
  have:  ε > 0,  x  S, d (Sup S) x < ε := begin
  intros ε ,
  obtain  x, hx, hs_lt  := this ε ,
  use x,
  split,
  exact hx,
  rw real.dist_eq,
  apply abs_lt_of_lt_of_neg_lt,
  exact hs_lt,
  sorry, -- by definition of sup.
  end,
  have:  (N: ),  x  S, d (Sup S) x < 1/(N + 1) := sorry,
  choose x hrange h using this,
  use x,
  split,
  intros y hy,
  obtain  N, hN  := hy,
  rw  hN,
  exact hrange N,
  intros ε ,
  -- 1/(N + 1) ≤ eps
  -- 1/eps ≤ N + 1
  -- 1/eps - 1 ≤ N
  lift floor(1/ε) to  with N₀,
  use N₀,
  intros n hn,
  transitivity,
  exact h n,
  sorry,
  end

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:54):

I can't find orderable in mathlib by the way

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:54):

Do you have a question or are you now OK to keep going?

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:55):

I think I can now finish the proof by myself —but feel free if you see stupid things (except the fact I'm writing my own metric_space def which is only for the sake of exercise.)

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 22:56):

Your proof looks just like the kind of proofs I was writing when I was learning.

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:58):

I definitely abuse of have because I'm trying to see how it works, but I clean up afterwards to have something more natural

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 22:59):

Other than this, I think I might be using obtain in a suboptimal way sometimes, and I'm not sure by what I should replace it

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 23:00):

transitivity is cool because it expresses 1:1 how I think, but those meta variables are not good I guess ; also, it does not work when I want to do: a ≤ b < c — I don't know what good replacement there would be for this? (I could chain the right lemmas given enough time, but it's somewhat annoying)

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 23:00):

lt_of_le_of_lt

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 23:01):

I should try to have the confidence to write those directly as they're so natural…

view this post on Zulip Mario Carneiro (Apr 03 2020 at 23:09):

it's actually order_topology

view this post on Zulip Mario Carneiro (Apr 03 2020 at 23:11):

I think the names changed at some point; there is order_topology and order_closed_topology now

view this post on Zulip Reid Barton (Apr 03 2020 at 23:13):

I also distinctly remember something about orderable

view this post on Zulip Scott Morrison (Apr 04 2020 at 02:27):

You can also use calc blocks instead of transitivity, or having the confidence to write lt_of_le_of_lt.

view this post on Zulip Scott Morrison (Apr 04 2020 at 02:28):

calc blocks also have the advantage of readability (as long as the proof terms on each line stay succinct).

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:14):

Ryan, do you know that transitivity can take an argument instantiating the meta-variable you complain about?

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:15):

I still agree with Scott that you should probably be using more calc blocks. linarith can also get rid of all this as long as you state the relevant fact before, or pass them to linarith.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:16):

@Patrick Massot I didn't know and I should have tried, I assumed that transitivity didn't take any argument, thanks.

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:16):

Your lemma sup_is_a_cv_seq was the end goal of my Lean L1 course last year.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:16):

Patrick Massot said:

I still agree with Scott that you should probably be using more calc blocks. linarith can also get rid of all this as long as you state the relevant fact before, or pass them to linarith.

I'll give a try to calc blocks, they look like more natural to me.

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:17):

But you are not approaching it in the right Lean mindset. You need to write the proof on paper, and collect all the « obvious facts » used in the proof. Them write lemmas about those obvious facts.

view this post on Zulip Kenny Lau (Apr 04 2020 at 09:17):

I don't like (set.range x) ⊆ S because it is harder to prove and use than \forall n, x n \in S

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:17):

Yes, I wanted to write this also.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:18):

Patrick Massot said:

Your lemma sup_is_a_cv_seq was the end goal of my Lean L1 course last year.

Oh wow, ideally, I'd like to generalize it to orderable topologies, like I'd been advised by @Mario Carneiro (behind this, I'm proving the classical Bolzano-Weierstrass)

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:18):

set.range and set.image are evil. They look nice on paper because you automatically do the required bureaucracy in your head without noticing.

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:19):

Sorry, I meant "of the exam of my Lean L1 course".

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:19):

Patrick Massot said:

set.range and set.image are evil. They look nice on paper because you automatically do the required bureaucracy in your head without noticing.

Kenny Lau said:

I don't like (set.range x) ⊆ S because it is harder to prove and use than \forall n, x n \in S

Alright, but stating \forall n, x n \in S looks like a bit weird when in reality what I want to express is that the image of the sequence is a subset of S

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:19):

I forgot part of the sentence.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:19):

Patrick Massot said:

I forgot part of the sentence.

Patrick Massot said:

Sorry, I meant "of the exam of my Lean L1 course".

Ah! Is it available somewhere? I'm quite interested into this!

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:19):

No, you want to express that the sequence takes values in S.

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:20):

You would never say "the image of the sequence is a subset of S".

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:20):

Indeed, I agree

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:21):

But I'd just write (xn)nSN(x_n)_n \in S^{\mathbb{N}}

view this post on Zulip Kenny Lau (Apr 04 2020 at 09:22):

but whenever you prove / use this sentence you always prove that xnSnx_n \in S \forall n

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:23):

Ryan Lahfa said:

But I'd just write (xn)nSN(x_n)_n \in S^{\mathbb{N}}

You shouldn't. Really.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:24):

Patrick Massot said:

Ryan Lahfa said:

But I'd just write (xn)nSN(x_n)_n \in S^{\mathbb{N}}

You shouldn't. Really.

What would you advise to write?

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:26):

Anyway, you should have lemma saying ∀ ε > 0, ∃ x ∈ S, Sup S - ε < x outside from your main proof. And then the same with 1/(N+1) instead of ε.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:28):

Patrick Massot said:

Anyway, you should have lemma saying ∀ ε > 0, ∃ x ∈ S, Sup S - ε < x outside from your main proof. And then the same with 1/(N+1) instead of ε.

Yes, I was planning to extract those as they're looking like lemmas on themselves.

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:28):

And a lemma saying that if for all n, d (x n) l < 1/(N+1) then x converges to l.

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:29):

Because these all lemmas that are "obvious" when you have already reached the point where you want to prove this Sup thing.

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:29):

So you don't want to be proving them in the middle of this proof.

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:29):

You wouldn't do that on paper and you wouldn't do that in Lean.

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:30):

And of course a lemma saying that 1/(N+1) is less than any epsilon for N large enough

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:33):

Definitely.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:33):

Would one_div_lt_epsilon be a right name for the last lemma?

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 09:34):

For forall n, d (x n) l < 1/(N + 1) → converge x l, I'm not sure how to call it except convergence_aux_1

view this post on Zulip Patrick Massot (Apr 04 2020 at 09:35):

converge_of_dist_lt_one_div_succ?

view this post on Zulip Kenny Lau (Apr 04 2020 at 09:35):

converge_of_d_lt

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 13:47):

I tried to take into account most of your advice and came back with this:

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X  X  )
(d_pos :  x y, d x y  0)
(presep :  x y, x = y  d x y = 0)
(sep :  x y, d x y = 0   x = y)
(sym :  x y, d x y = d y x)
(triangle :  x y z, d x z  d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

instance real.metric_space : metric_space  :=
{ d                  := λx y, abs (x - y),
  d_pos              := by simp [abs_nonneg],
  presep             := begin simp, apply sub_eq_zero_of_eq end,
  sep                := begin simp, apply eq_of_sub_eq_zero end,
  sym                := assume x y, abs_sub _ _,
  triangle           := assume x y z, abs_sub_le _ _ _ }

theorem real.dist_eq (x y : ) : d x y = abs (x - y) := rfl

theorem real.dist_0_eq_abs (x : ) : d x 0 = abs x :=
by simp [real.dist_eq]

def converge (x:   X) (l : X) :=
   ε > 0,  N,  n  N, ((d l (x n))  < ε)

lemma real.sup_sub_lt_eps {S: set }:  ε > 0,  x  S, Sup S - x < ε := sorry
lemma real.sup_dist_lt_eps {S: set }:  ε > 0,  x  S, d (Sup S) x < ε := begin
  intros ε ,
  obtain  x, hx, hs_lt  := real.sup_sub_lt_eps ε ,
  use x,
  split,
  exact hx,
  rw real.dist_eq,
  apply abs_lt_of_lt_of_neg_lt,
  exact hs_lt,
  sorry,
end

lemma converge_of_dist_lt_one_div_succ {x:   } {l: }: ( n, d l (x n)  1 / (n + 1))  converge x l := begin
intro H,
intros ε ,
obtain  N, hN  := exists_nat_one_div_lt ,
use N,
intros n hn,
calc d l (x n)  1 / (n + 1) : H n
    ...  1 / (N + 1) : nat.one_div_le_one_div hn
    ... < ε : hN
end

lemma sup_is_a_cv_seq (S: set ):
  S.nonempty  bdd_above S   (x:   ), ( n, x n  S)  converge x (Sup S) := begin
  intros hnn hbdd,
  have:  (N: ),  x  S, d (Sup S) x < 1/(N + 1) := begin
  intro N,
  apply real.sup_dist_lt_eps,
  apply nat.one_div_pos_of_nat,
  end,
  choose x hrange h using this,
  use x,
  split,
  exact hrange,
  exact converge_of_dist_lt_one_div_succ h, -- this line should work (?)
  end

But, I have some issue regarding the types, here is the state at the last step:

type mismatch at application
  converge_of_dist_lt_one_div_succ h
term
  h
has type
   (N : ), d (Sup S) (x N) < 1 / (N + 1)
but is expected to have type
   (n : ), d (Sup S) (x n)  1 / (n + 1)
state:
S : set ,
hnn : set.nonempty S,
hbdd : bdd_above S,
x :   ,
hrange :  (N : ), x N  S,
h :  (N : ), d (Sup S) (x N) < 1 / (N + 1)
 converge x (Sup S)

I'm not sure what is actually different except some typeclasses, I tried to print those with set_option pp.all true but got lost as there were a huge amount of those.

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 13:49):

You have a < in one and a <=in the other

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 13:49):

Thanks…

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 13:51):

@Kevin Buzzard Is there a way to apply le_of_lt in this part:

  have:  (N: ),  x  S, d (Sup S) x  1/(N + 1) := begin
  intro N,
  apply le_of_lt, -- won't work because of exists
  apply real.sup_dist_lt_eps,
  apply nat.one_div_pos_of_nat,
  end,

?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 13:56):

Instead of apply use convert maybe. What is the type of real.sup_dist_lt_pos?

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 13:56):

Kevin Buzzard said:

Instead of apply use convert maybe. What is the type of real.sup_dist_lt_pos?

lemma real.sup_dist_lt_eps {S: set ℝ}: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := begin

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 13:57):

Make a term which starts with an exists from that term and convert it

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 13:58):

Ie supply the correct epsilon

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 13:58):

Hmm this still won't work

view this post on Zulip Reid Barton (Apr 04 2020 at 13:58):

right, it won't work because le_of_lt is not an equality

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 13:59):

I tried this: convert real.sup_dist_lt_eps (1 / (N + 1)) (nat.one_div_pos_of_nat),

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 13:59):

Well just do cases on the term to get to an epsilon

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 13:59):

Convert won't work

view this post on Zulip Reid Barton (Apr 04 2020 at 13:59):

You need to know if P(x)    Q(x)P(x) \implies Q(x) for all x, then (x,P(x))    (x,Q(x))(\exists x, P(x)) \implies (\exists x, Q(x)) and we don't have a general framework for that

view this post on Zulip Reid Barton (Apr 04 2020 at 13:59):

If it was == and not     \implies then you could use convert or conv or whatever.

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:00):

Do cases on the term you make with the exists and use that x

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:02):

Or just apply the logic lemma. Presumably it's in logic.basic?

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:02):

Kevin Buzzard said:

Well just do cases on the term to get to an epsilon

Is this something like this: cases (real.sup_dist_lt_eps (1 / (N + 1)) (nat.one_div_pos_of_nat)) with x hx, often?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:03):

If you got an x and an hx that looks good then yes. You might be better off with rcases though

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:04):

Because you want to extract x in S and not just x

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:04):

Is there a preference between rcases and obtain?

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:04):

Because I often use obtain to extract arbitrary complex constructors

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:05):

Obtain is best

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:05):

This works:

  have:  (N: ),  x  S, d (Sup S) x  1/(N + 1) := begin
  intro N,
  obtain  x, hrange, hsup  := (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat)),
  use x,
  split,
  exact hrange,
  apply le_of_lt,
  exact hsup,
  end,

anyway

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:05):

I always forget about it because it's relatively new

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:05):

Thanks!

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:06):

Now can you write it in pure term mode?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:06):

lambda instead of intro etc?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:07):

There are no serious tactics in your code so you don't need tactic mode at all

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:07):

Obtain becomes let ... in

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:07):

Split is pointy brackets

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:07):

And exact can be removed completely

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:08):

I started like this: λ N, let ⟨ x, hrange, hsup ⟩ in (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat)),

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:08):

But it is complaining about the syntax — I guess I'm doing something wrong

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:09):

Huh, yes let x := t in s

view this post on Zulip Patrick Massot (Apr 04 2020 at 14:09):

Your use of obtain make it completely equivalent to rcases. This is fine, but you should know the added value of obtain is you can write the expected type upfront.

view this post on Zulip Patrick Massot (Apr 04 2020 at 14:10):

In your case that would be purely for readability purposes.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:11):

Patrick Massot said:

Your use of obtain make it completely equivalent to rcases. This is fine, but you should know the added value of obtain is you can write the expected type upfront.

I see, I can do obtain <pattern>: type := … and I can omit <pattern> ?

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:12):

@Kevin Buzzard I'm not sure how to replace the use x; (also is there any docs for the commands for the pointy brackets, etc. ?)

view this post on Zulip Patrick Massot (Apr 04 2020 at 14:13):

You can do a lot of things:

  obtain x, hx :  x, P x,
  { long proof... },
  obtain x, hx :  x, P x := proof_term,
  obtain x, hx :  x, P x, from proof_term,

view this post on Zulip Patrick Massot (Apr 04 2020 at 14:14):

Only the first case really needs obtain rather than rcases. But all are more readable than rcases

view this post on Zulip Patrick Massot (Apr 04 2020 at 14:14):

And of course you can get the same with have + rcases but you'd get tired of this pretty quickly.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:16):

Makes sense, is there any docs to write tactics? I'm understanding more and more how to compose all of this and I'm interested in how it works

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:23):

Beginning tactic writing is covered in a doc which Patrick wrote in the docs directory of mathlib

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:28):

Now I'm this far:

have:  (N: ),  x  S, d (Sup S) x  1/(N + 1) := λ N,
  let  x, ha, hb  := (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat))
  in exists.intro x (λ hp, and.intro (...) (...) ),

Is it expected that Lean VSCode cannot print the current state in term mode?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:29):

Use X is just <X,_> with the right brackets

view this post on Zulip Bhavik Mehta (Apr 04 2020 at 14:29):

By the way, can we make VSCode highlight obtain (and set) the same way as have (and let)?

view this post on Zulip Reid Barton (Apr 04 2020 at 14:30):

Use _ where you have (...), and then hover over it, or something (I use emacs, but I assume vscode can do this too)

view this post on Zulip Gabriel Ebner (Apr 04 2020 at 14:31):

@Bhavik Mehta Feel free to PR a change to this file: https://github.com/leanprover/vscode-lean/blob/9a4400a1f3db57d0a25c1944812b0c2dc9ff2141/syntaxes/lean.json#L35 But I wouldn't highlight set: this occurs often as a non-tactic, e.g. in set α.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:31):

Indeed, it works when I use _, now I have this state:

context:
S : set ,
hnn : set.nonempty S,
hbdd : bdd_above S,
N : ,
_let_match :
  ( (x : ) (H : x  S), d (Sup S) x < 1 / (N + 1)) 
  ( (x : ) (H : x  S), d (Sup S) x  1 / (N + 1)),
x : ,
ha : x  S,
hb : d (Sup S) x < 1 / (N + 1)
  (H : x  S), d (Sup S) x  1 / (N + 1)

But the exists in front of this is strange? I'm not sure how I can combine ha/hb to finish

view this post on Zulip Bhavik Mehta (Apr 04 2020 at 14:32):

Gabriel Ebner said:

Bhavik Mehta Feel free to PR a change to this file: https://github.com/leanprover/vscode-lean/blob/9a4400a1f3db57d0a25c1944812b0c2dc9ff2141/syntaxes/lean.json#L35 But I wouldn't highlight set: this occurs often as a non-tactic, e.g. in set α.

Thanks! Ah yeah good point

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:32):

have:  (N: ),  x  S, d (Sup S) x  1/(N + 1) := λ N,
  let  x, ha, hb  := (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat))
  in  x,  ha, le_of_lt hb  ,

This seems to work!

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:34):

Thank you for the tip! I have seen symbols like , what does that mean? I see it in mathlib sometimes, but I didn't find any docs on it

view this post on Zulip Reid Barton (Apr 04 2020 at 14:34):

ah, the dreaded "stupid triangle"

view this post on Zulip Patrick Massot (Apr 04 2020 at 14:36):

also known by its full name as the dreaded "I'm-sorry-but-I-don't-know-the-expected-type triangle".

view this post on Zulip Reid Barton (Apr 04 2020 at 14:37):

if p : P a and e : a = b then e ▸ p : P b, except it basically never manages to work out what P should be

view this post on Zulip Reid Barton (Apr 04 2020 at 14:37):

it's like a term-mode version of rw that rarely works

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:37):

Oh okay

view this post on Zulip Patrick Massot (Apr 04 2020 at 14:38):

You get extra credit when you manage to use it in a proof.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 14:38):

Hahahaha

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:44):

Good job for getting the term!

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 14:46):

One thing to remember about the stupid triangle is that in contrast to tactic mode it has to be told all inputs , ie rw add_comm works but with the triangle you might have to put add_comm a b


Last updated: May 10 2021 at 08:14 UTC