feat (analysis/topology): implement sequential spaces and sequential continuity, show metric spaces are sequential #440

jdsalchow · 2018-10-23T14:14:59Z

feat (analysis/topology): implement sequential spaces and sequential continuity, show metric spaces are sequential

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

robertylewis

This looks very clean! The ‹ › notation isn't used so much in mathlib, and this is certainly verbose, but that's not necessarily bad. This is very legible to me.

Here are some quick stylistic comments. Many of them apply to multiple places in the file, you should be able to find where pretty quickly. I'm also trying out Github's suggestion feature, which I've never used...

analysis/topology/sequences.lean

robertylewis · 2018-10-23T15:14:46Z

analysis/topology/sequences.lean

+                                                      metrically_converges_to_iff_converges_to
+                                 ... ↔ tendsto x at_top (nhds limit) : converges_to_iff_tendsto
+
+private lemma one_div_succ_pos (n : ℕ) : 1 / ((n : ℝ) + 1) > 0 :=


I think I did this originally, but this should probably be moved somewhere more general.

Yep, it's a copy of your private lemma from the Cauchy sequence filter file. Any suggestions as to where a non private version of this can go? I was tempted to put it into real.lean, but the statement is true in a more general context.

algebra/ordered_field.lean?

That seems wrong as it would imply importing the reals in ordered field.

This should work more generally for some ordered fields

analysis/topology/sequences.lean

robertylewis · 2018-10-23T15:18:42Z

analysis/topology/sequences.lean

+  -- from this, construct a "sequence of hypothesis" h, (h n) := _ ∈ {x // x ∈ ball (1/n+1) p ∩ M}
+  let h := λ n : ℕ, (classical.indefinite_description _ (set.exists_mem_of_ne_empty (this n))) in
+  -- an actual sequence
+  let x := λ n : ℕ, (h n).val in


You can combine two lets into one:

let h := _, x := _ in

robertylewis · 2018-10-23T15:22:16Z

analysis/topology/sequences.lean

+-- necessary for the next instance
+set_option eqn_compiler.zeta true
+/- Show that every metric space is sequential. -/
+instance metric_space.to_sequential_space: sequential_space X :=


space before colon (otherwise the VS Code highlighting is off)

Suggested change

instance metric_space.to_sequential_space: sequential_space X :=

instance metric_space.to_sequential_space : sequential_space X :=

@robertylewis Thanks for the bug report! It's fixed now.

Heh, I guess I could have made this bug report easier to find.... Thanks!

analysis/topology/sequences.lean

jcommelin · 2018-10-23T17:04:25Z

This certainly looks very readable! I should learn to write term-mode proofs like this!

jcommelin · 2018-10-23T17:06:05Z

analysis/topology/sequences.lean

+ - (*) define the sequential closure of a set and prove that it's contained in the closure, 
+ - (*) define a type class "sequential_space" in which closure and sequential closure agree, 
+ - (*) define sequential continuity and show that it coincides with continuity in sequential spaces,
+ - (*) provide and instance that shows that every metric space is a sequential space.


Suggested change

- (*) provide and instance that shows that every metric space is a sequential space.

- (*) provide an instance that shows that every metric space is a sequential space.

jcommelin · 2018-10-23T17:08:01Z

analysis/topology/sequences.lean

+
+/- The notion of convergence of sequences in topological spaces. -/
+def converges_to (x : ℕ → X) (limit : X) : Prop :=
+  ∀ U : set X, limit ∈ U → is_open U → ∃ n0 : ℕ, ∀ n ≥ n0, (x n) ∈ U


I guess I would personally swap the order of the hypotheses: first assume that U is open, and then assume that the limit is in U. But that is certainly a matter of taste.

I don't have much of a preference either way.

jcommelin · 2018-10-23T17:13:29Z

analysis/topology/sequences.lean

+    let ⟨x, ⟨_, _⟩⟩ := this in
+    show p ∈ A, from h x ‹∀ n : ℕ, ((x n) ∈ A)› p ‹converges_to x p›))
+
+/- The sequential closure of a set is containt in the closure of that set. The converse is not


Suggested change

/- The sequential closure of a set is containt in the closure of that set. The converse is not

/- The sequential closure of a set is contained in the closure of that set. The converse is not

kckennylau · 2018-11-11T17:52:02Z

Is there anything wrong with this PR?

johoelzl · 2018-11-13T17:27:04Z

I hope to find some in one or two weeks. I'm a little bit occupied with preparing a lecture and reviews.

jdsalchow · 2018-12-12T12:41:42Z

What's the state of this?

analysis/topology/sequences.lean

rwbarton · 2018-12-15T04:32:42Z

analysis/topology/sequences.lean

+show p ∈ closure M, from
+-- we have to show that p is in the closure of M
+-- using mem_closure_iff, this is equivalent to proving that every open neighbourhood
+-- has nonempty intersection with A, but this is witnessed by our sequence x


M turned into A in the comment. Might be worth going through and changing all the As to M or vice versa.

rwbarton · 2018-12-15T04:37:45Z

analysis/topology/sequences.lean

+-- using mem_closure_iff, this is equivalent to proving that every open neighbourhood
+-- has nonempty intersection with A, but this is witnessed by our sequence x
+suffices ∀ O, is_open O → p ∈ O → O ∩ M ≠ ∅, from mem_closure_iff.mpr this,
+assume O is_open_O O_cap_M_neq_empty,


Suggested change

assume O is_open_O O_cap_M_neq_empty,

assume O is_open_O p_in_O,

That would be misleading, in general p is only in the sequential closure of M, not in M.

O_cap_M_neq_empty sounds like the type is O ∩ M ≠ ∅, but it is p ∈ O

analysis/topology/sequences.lean

rwbarton · 2018-12-15T04:51:50Z

analysis/topology/sequences.lean

+                                                      metrically_converges_to_iff_converges_to
+                                 ... ↔ tendsto x at_top (nhds limit) : converges_to_iff_tendsto
+
+private lemma one_div_succ_pos (n : ℕ) : 1 / ((n : ℝ) + 1) > 0 :=


algebra/ordered_field.lean?

johoelzl

@jdsalchow sorry for the long delay. Generally we try to use tendsto and not introduce too much additional constants.

johoelzl · 2019-01-11T17:42:59Z

analysis/topology/sequences.lean

+-- using mem_closure_iff, this is equivalent to proving that every open neighbourhood
+-- has nonempty intersection with A, but this is witnessed by our sequence x
+suffices ∀ O, is_open O → p ∈ O → O ∩ M ≠ ∅, from mem_closure_iff.mpr this,
+assume O is_open_O O_cap_M_neq_empty,


O_cap_M_neq_empty sounds like the type is O ∩ M ≠ ∅, but it is p ∈ O

johoelzl · 2019-01-11T17:44:55Z

analysis/topology/sequences.lean

+universes u v
+variables {X : Type u} {Y : Type v}
+
+def to_filter (x : ℕ → X) : filter X := filter.map x at_top


this is never used

johoelzl · 2019-01-11T17:46:31Z

analysis/topology/sequences.lean

+variables [topological_space X] [topological_space Y]
+
+/-- The notion of convergence of sequences in topological spaces. -/
+def converges_to (x : ℕ → X) (limit : X) : Prop :=


This definition is not necessary. It would be nice to have a notation for this, and prove converges_to_iff_tendsto in the other way round.

What do you mean by 'the other way around'? Just the symmetric statement i.e. converges_to_iff_tendsto?

The idea is to avoid introducing too many new concepts for slight variations of the same notion. It makes the library confusing; for example, converges_to might mean any of a number of things. You should use tendsto x at_top (nhds limit) directly rather than the new concept, converges_to. The lemma should then assert that tendsto x at_top (nhds limit) is equivalent to the current definition of converges_to.

Also, doesn't the equivalence hold for an arbitrary preorder, not just nat?

johoelzl · 2019-01-11T17:47:39Z

analysis/topology/sequences.lean

+                                             (mem_nhds_sets isOpenU limitInU),
+        show ∃ n0 : ℕ, ∀ n ≥ n0, (x n) ∈ U, from mem_at_top_sets.mp this)
+
+/--


remove the - in the next two lines. They occur in the tooltip, i.e, the tooltip is now - The sequential closure of a subset M ⊆ X of a topological space X is - the set of all p ∈ X which arise as limit of sequences in M.

johoelzl · 2019-01-11T17:47:50Z

analysis/topology/sequences.lean

+      show p ∈ A, from h x ‹∀ n : ℕ, ((x n) ∈ A)› p ‹converges_to x p›))
+
+/--
+ - The sequential closure of a set is contained in the closure of that set. The converse is not


ditto for -

johoelzl · 2019-01-11T17:48:49Z

analysis/topology/sequences.lean

+is_mem_of_conv_to_of_is_seq_closed (is_seq_closed_of_is_closed A ‹is_closed A›)
+  ‹∀ n, x n ∈ A› ‹converges_to x limit›
+
+/--


ditto for -

johoelzl · 2019-01-11T17:55:27Z

analysis/topology/sequences.lean

+
+/-- The usual notion of convergence of sequences in metric spaces. -/
+def metrically_converges_to (x : ℕ → X) (limit : X) : Prop :=
+∀ ε > 0, ∃ n0 : ℕ, ∀ n ≥ n0, dist (x n) limit < ε


same as converges_to, i.e. remove this definition

johoelzl · 2019-01-11T17:56:18Z

analysis/topology/sequences.lean

+                                                      metrically_converges_to_iff_converges_to
+                                 ... ↔ tendsto x at_top (nhds limit) : converges_to_iff_tendsto
+
+private lemma one_div_succ_pos (n : ℕ) : 1 / ((n : ℝ) + 1) > 0 :=


This should work more generally for some ordered fields

avigad · 2019-01-15T15:29:37Z

@jdsalchow Thank you for these theorems and definitions. They look very good to me, but there is one thing that should be improved.

I just confirmed that two of the main lemmas, topological_space.seq_tendsto_iff and metrtic_space.seq_tendsto_iff go through exactly as they are if you declare

variables {γ : Type*} [semilattice_sup γ] [inhabited γ]

and replace ℕ by γ everywhere. In other words, they have nothing to do with sequences. They work just as well for functions from the reals, for example. They are useful characterizations of convergence at infinity, and should be stated in full generality.

I would recommend naming them topological_space.tendsto_at_top_iff and metric_space.tendsto_at_top_iff and moving them to the files topological_space and metric_space, respectively.

(If you are feeling energetic, it would be nice to have the corresponding theorems for at_bot, but I would not insist on it for the PR.)

Co-Authored-By: jdsalchow <jdsalchow@gmail.com>

jdsalchow · 2019-01-20T13:29:41Z

I just confirmed that two of the main lemmas, topological_space.seq_tendsto_iff and metrtic_space.seq_tendsto_iff go through exactly as they are if you declare
variables {γ : Type*} [semilattice_sup γ] [inhabited γ]
and replace ℕ by γ everywhere. In other words, they have nothing to do with sequences. They work just as well for functions from the reals, for example. They are useful characterizations of convergence at infinity, and should be stated in full generality.

@avigad If I do that, the two lemmas would have to move out of the file about sequences, and be put into a logical context that fits such a general lemma. Then those two lemmas would need to be restated as a corollary of the general thing.

I'm happy to do that, if there is a place in which the more general statements would fit. Otherwise, I suggest to put a comment there, indicating that the proofs generalise. Then the first person who needs it can do this (trivial) generalisation.

jdsalchow · 2019-01-20T14:48:53Z

Is this failing because of some olean caching issue? It builds fine locally ...

digama0 · 2019-01-21T01:39:45Z

some files got moved around - analysis.topology.* is now topology.*. Check your imports

…ty (closes #440) Co-Authored-By: Reid Barton <rwbarton@gmail.com>

robertylewis reviewed Oct 23, 2018

View reviewed changes

jcommelin reviewed Oct 23, 2018

View reviewed changes

analysis/topology/sequences.lean Outdated Show resolved Hide resolved

jcommelin reviewed Oct 23, 2018

View reviewed changes

rwbarton reviewed Dec 15, 2018

View reviewed changes

jdsalchow force-pushed the sequences branch from 97783cd to 5b04ba9 Compare December 18, 2018 10:44

johoelzl reviewed Jan 11, 2019

View reviewed changes

jdsalchow force-pushed the sequences branch 2 times, most recently from b787b7c to f07478c Compare January 15, 2019 14:35

jdsalchow and others added 12 commits January 20, 2019 14:11

sequences, sequential spaces, and sequential continuity

6a5e4d3

fixed notation

db01e53

more notation

6d5f8db

fixed typos

fb15076

Update analysis/topology/sequences.lean

df1e94b

Co-Authored-By: jdsalchow <jdsalchow@gmail.com>

Update analysis/topology/sequences.lean

1ed1804

Co-Authored-By: jdsalchow <jdsalchow@gmail.com>

Update analysis/topology/sequences.lean

8cdcda4

Co-Authored-By: jdsalchow <jdsalchow@gmail.com>

Update analysis/topology/sequences.lean

8aab4a9

Co-Authored-By: jdsalchow <jdsalchow@gmail.com>

Update analysis/topology/sequences.lean

fa64ff3

Co-Authored-By: jdsalchow <jdsalchow@gmail.com>

Implement changes suggested by rwbarton.

1a1faa9

Update to upstream.

2555e95

Implement changes requested.

8293bc2

jdsalchow force-pushed the sequences branch from f07478c to 8293bc2 Compare January 20, 2019 14:01

rename file

e5ce4ba

johoelzl closed this in 4018daf Jan 23, 2019

cipher1024 pushed a commit that referenced this pull request Feb 8, 2019

feat(topology): sequences, sequential spaces, and sequential continui…

6a1c1f4

…ty (closes #440) Co-Authored-By: Reid Barton <rwbarton@gmail.com>

	instance metric_space.to_sequential_space: sequential_space X :=
	instance metric_space.to_sequential_space : sequential_space X :=

	- (*) provide and instance that shows that every metric space is a sequential space.
	- (*) provide an instance that shows that every metric space is a sequential space.

	/- The sequential closure of a set is containt in the closure of that set. The converse is not
	/- The sequential closure of a set is contained in the closure of that set. The converse is not

	assume O is_open_O O_cap_M_neq_empty,
	assume O is_open_O p_in_O,

feat (analysis/topology): implement sequential spaces and sequential continuity, show metric spaces are sequential #440

feat (analysis/topology): implement sequential spaces and sequential continuity, show metric spaces are sequential #440

Conversation

jdsalchow commented Oct 23, 2018

robertylewis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcommelin commented Oct 23, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kckennylau commented Nov 11, 2018

johoelzl commented Nov 13, 2018

jdsalchow commented Dec 12, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

johoelzl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

avigad commented Jan 15, 2019

jdsalchow commented Jan 20, 2019

jdsalchow commented Jan 20, 2019

digama0 commented Jan 21, 2019