## Stream: maths

### Topic: Link between sequential and epsilon/delta versions

#### 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 $a$ of a sequence $x$:

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

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

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

Continuity:
We say that $f : A \to B$ is continuous at $x \in A$ if:

Epsilon/delta: $\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: $\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)$

#### Mario Carneiro (Apr 03 2020 at 19:35):

Filters are the unifying abstraction here

#### 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

#### 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

#### 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

#### 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)

#### 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!

#### 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

#### Mario Carneiro (Apr 03 2020 at 19:44):

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

#### Ryan Lahfa (Apr 03 2020 at 19:46):

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

#### 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?

#### Alex J. Best (Apr 03 2020 at 20:00):

classical.skolem in core lean?

#### 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

#### 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?

#### 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 (?).

#### Patrick Massot (Apr 03 2020 at 20:21):

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

#### 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…

#### 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.

#### 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!

#### 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?

#### 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 ε hε,
-- 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.

#### 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.

#### Ryan Lahfa (Apr 03 2020 at 22:12):

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

#### 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 ε hε,
-- 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.

#### 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

#### 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!

#### Kevin Buzzard (Apr 03 2020 at 22:31):

I am concerned about your first sorry

#### Mario Carneiro (Apr 03 2020 at 22:31):

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

#### Kevin Buzzard (Apr 03 2020 at 22:31):

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

#### 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.

#### 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.

#### Mario Carneiro (Apr 03 2020 at 22:32):

but the definition doesn't say anything about sequences

#### 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)

#### 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.

#### Kevin Buzzard (Apr 03 2020 at 22:33):

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

#### 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?

#### Kevin Buzzard (Apr 03 2020 at 22:33):

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

#### Ryan Lahfa (Apr 03 2020 at 22:33):

Mario Carneiro said:

but the definition doesn't say anything about sequences

Of metric spaces?

#### 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.

#### Mario Carneiro (Apr 03 2020 at 22:34):

I think you want to know that the topology is orderable

#### Kevin Buzzard (Apr 03 2020 at 22:34):

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

#### 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

#### 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"

#### Ryan Lahfa (Apr 03 2020 at 22:39):

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

#### Ryan Lahfa (Apr 03 2020 at 22:41):

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

#### Kevin Buzzard (Apr 03 2020 at 22:51):

If you don't want to work with $\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.

#### 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.

#### Ryan Lahfa (Apr 03 2020 at 22:53):

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

#### 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 ε hε,
obtain ⟨ x, hx, hs_lt ⟩ := this ε hε,
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 ε hε,
-- 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


#### Kevin Buzzard (Apr 03 2020 at 22:54):

I can't find orderable in mathlib by the way

#### Kevin Buzzard (Apr 03 2020 at 22:54):

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

#### 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.)

#### Kevin Buzzard (Apr 03 2020 at 22:56):

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

#### 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

#### 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

#### 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)

#### Kevin Buzzard (Apr 03 2020 at 23:00):

lt_of_le_of_lt

#### Ryan Lahfa (Apr 03 2020 at 23:01):

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

#### Mario Carneiro (Apr 03 2020 at 23:09):

it's actually order_topology

#### 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

#### Reid Barton (Apr 03 2020 at 23:13):

I also distinctly remember something about orderable

#### 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.

#### 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).

#### 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?

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### 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

#### Patrick Massot (Apr 04 2020 at 09:17):

Yes, I wanted to write this also.

#### 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)

#### 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.

#### Patrick Massot (Apr 04 2020 at 09:19):

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

#### 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

#### Patrick Massot (Apr 04 2020 at 09:19):

I forgot part of the sentence.

#### 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!

#### Patrick Massot (Apr 04 2020 at 09:19):

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

#### Patrick Massot (Apr 04 2020 at 09:20):

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

Indeed, I agree

#### Ryan Lahfa (Apr 04 2020 at 09:21):

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

#### Kenny Lau (Apr 04 2020 at 09:22):

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

#### Patrick Massot (Apr 04 2020 at 09:23):

Ryan Lahfa said:

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

You shouldn't. Really.

#### Ryan Lahfa (Apr 04 2020 at 09:24):

Patrick Massot said:

Ryan Lahfa said:

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

You shouldn't. Really.

What would you advise to write?

#### 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 ε.

#### 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.

#### 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.

#### 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.

#### Patrick Massot (Apr 04 2020 at 09:29):

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

#### Patrick Massot (Apr 04 2020 at 09:29):

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

#### 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

Definitely.

#### Ryan Lahfa (Apr 04 2020 at 09:33):

Would one_div_lt_epsilon be a right name for the last lemma?

#### 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

#### Patrick Massot (Apr 04 2020 at 09:35):

converge_of_dist_lt_one_div_succ?

#### Kenny Lau (Apr 04 2020 at 09:35):

converge_of_d_lt

#### 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 ε hε,
obtain ⟨ x, hx, hs_lt ⟩ := real.sup_sub_lt_eps ε hε,
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 ε hε,
obtain ⟨ N, hN ⟩ := exists_nat_one_div_lt hε,
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.

#### Kevin Buzzard (Apr 04 2020 at 13:49):

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

Thanks…

#### 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,


?

#### Kevin Buzzard (Apr 04 2020 at 13:56):

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

#### 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

#### Kevin Buzzard (Apr 04 2020 at 13:57):

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

#### Kevin Buzzard (Apr 04 2020 at 13:58):

Ie supply the correct epsilon

#### Kevin Buzzard (Apr 04 2020 at 13:58):

Hmm this still won't work

#### Reid Barton (Apr 04 2020 at 13:58):

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

#### 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),

#### Kevin Buzzard (Apr 04 2020 at 13:59):

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

#### Kevin Buzzard (Apr 04 2020 at 13:59):

Convert won't work

#### Reid Barton (Apr 04 2020 at 13:59):

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

#### Reid Barton (Apr 04 2020 at 13:59):

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

#### Kevin Buzzard (Apr 04 2020 at 14:00):

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

#### Kevin Buzzard (Apr 04 2020 at 14:02):

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

#### 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?

#### 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

#### Kevin Buzzard (Apr 04 2020 at 14:04):

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

#### Ryan Lahfa (Apr 04 2020 at 14:04):

Is there a preference between rcases and obtain?

#### Ryan Lahfa (Apr 04 2020 at 14:04):

Because I often use obtain to extract arbitrary complex constructors

Obtain is best

#### 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

#### Kevin Buzzard (Apr 04 2020 at 14:05):

I always forget about it because it's relatively new

Thanks!

#### Kevin Buzzard (Apr 04 2020 at 14:06):

Now can you write it in pure term mode?

#### 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

#### Kevin Buzzard (Apr 04 2020 at 14:07):

Obtain becomes let ... in

#### Kevin Buzzard (Apr 04 2020 at 14:07):

Split is pointy brackets

#### Kevin Buzzard (Apr 04 2020 at 14:07):

And exact can be removed completely

#### 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)),

#### Ryan Lahfa (Apr 04 2020 at 14:08):

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

#### Ryan Lahfa (Apr 04 2020 at 14:09):

Huh, yes let x := t in s

#### 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.

#### 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> ?

#### 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. ?)

#### 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,


#### 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

#### 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.

#### 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

#### 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

#### 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?

#### Kevin Buzzard (Apr 04 2020 at 14:29):

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

#### 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)?

#### 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)

#### 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 α.

#### 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

#### 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

#### 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!

#### 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

#### 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".

#### 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

#### Reid Barton (Apr 04 2020 at 14:37):

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

Oh okay

#### Patrick Massot (Apr 04 2020 at 14:38):

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

Hahahaha

#### Kevin Buzzard (Apr 04 2020 at 14:44):

Good job for getting the term!

#### 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