Sequences in topological/metric spaces

Stream: general

[Rohan Mitta]

Hi,

I'm trying to prove some propositions about complete metric spaces and need to use sequences for them. I can't seem to find any lemmas in topological_space or metric_space to do with sequences, and was wondering if I should be trying to prove my own basic lemmas about sequences or if I missed something. I also wonder if I'm thinking about sequences properly.

For example, below I wanted to prove that if Y is a subset of a metric space, and y is an element of the closure of Y, then there exists a sequence in Y converging to y. Am I approaching this correctly?

import analysis.metric_space
import order.filter

theorem lim_sequence_of_mem_closure {α : Type*} [metric_space α] (Y : set α) (a : α) (H : a ∈ closure Y) :
∃ (f : ℕ → α) (H1 : ∀ (n : ℕ), f n ∈ Y), filter.tendsto f filter.cofinite (nhds a)  := begin
  have := mem_closure_iff_nhds.1 H,
  let ball_n := λ (n : ℕ), ball a ((1 : ℝ)/n),

  have H1 : ∀ (n : ℕ), nonempty {x : α | x ∈ (ball_n (n+1)) ∩ Y},
    intro n,
    apply @nonempty_of_exists _ (λ _,true),
    have H2 := this (ball_n (n+1)) (ball_mem_nhds _ _),
    have H3 := set.exists_mem_of_ne_empty H2,
    cases H3 with xn Hxn,
    existsi (⟨xn, Hxn⟩ : ↥{x : α | x ∈ ball_n (n+1) ∩ Y}),
    trivial,
    sorry,

  have sequence := λ (n : ℕ), classical.choice (H1 n),
  let sequencevals := λ (n : ℕ), (sequence n).val,
  existsi sequencevals,
  have H1 : ∀ (n : ℕ), sequencevals n ∈ Y,
    show ∀ (n : ℕ), (sequence n).val ∈ Y,
    let sequenceprops := λ (n : ℕ), ((sequence n).property).2,
    exact sequenceprops,
  existsi H1,
  sorry,

end

[Mario Carneiro]

I think we would want to state this over first countable spaces instead of metric spaces. What are you using it for?

[Rohan Mitta]

I want to use it to help me show that a complete subspace Y of a metric space X is closed in X

[Rohan Mitta]

I'm working towards eventually proving Banach's fixed point theorem but am starting with some easier propositions about complete metric spaces

[Patrick Massot]

I'm pretty sure the first thing is already there

[Patrick Massot]

but maybe not

[Mario Carneiro]

complete subspace Y of a metric space X is closed in X

This has nothing to do with sequences, it generalizes to uniform spaces

[Mario Carneiro]

It's not the same as your statement, but this lemma writes out the definition of complete so that we can say "a complete subspace Y of X"

lemma compact_of_totally_bounded_complete {s : set α}
  (ht : totally_bounded s) (hc : ∀{f:filter α}, cauchy f → f ≤ principal s → ∃x∈s, f ≤ nhds x) :
  compact s :=

[Mario Carneiro]

This is what I recommend proving:

variables {α : Type*} [uniform_space α]
lemma is_closed_of_complete {s : set α}
  (hc : ∀{f:filter α}, cauchy f → f ≤ principal s → ∃x∈s, f ≤ nhds x) :
  is_closed s :=

[Rohan Mitta]

Okay, I see, I'll try that. Thanks!
I've still got somewhat of a problem because I can't see a way around using sequences for the proof of Banach's fixed point theorem, so I will need to eventually find a good way of dealing with them in order to do that. That can be a task for later at this point though.

[Mario Carneiro]

The banach fixed point theorem looks pretty tied to metric spaces. I'm not sure how you could state it for uniform spaces. One possibility is some kind of well ordered filtration of the elements of the uniformity such that the contraction mapping forward maps each entourage to one that is strictly greater in the well order. That is, you have a antitone map o from entourages to ordinals such that if S is an entourage, then o (map F S) > o S

[Patrick Massot]

Are you trying to help him or scare him?

[Mario Carneiro]

...that said, I think you should just try to prove the regular BFP on metric spaces

[Patrick Massot]

Is your definition of a complete subspace of a uniform space equivalent to asking the induced uniformity is complete?

[Mario Carneiro]

yes

[Patrick Massot]

it seems so

[Mario Carneiro]

we will probably want a proof of equivalence, but I'm not sure how hard the statement is

[Mario Carneiro]

I guess complete_space s is a Prop so that should work

[Mario Carneiro]

Then again, we have the theorem complete_space s <-> is_closed s so I guess the latter is a simpler way to write it :)

[Patrick Massot]

For Rohan, I would say that relevant lemmas as cauchy_vmap in uniform_space.lean and is_closed_iff_nhds in topological_space.lean

[Patrick Massot]

What?

[Patrick Massot]

Which theorem?

[Mario Carneiro]

I mean once Rohan proves it

[Patrick Massot]

ah ok

[Rohan Mitta]

Thanks so much both of you! I'm going to sleep now but I'll see what I can do on it over the weekend.

[Patrick Massot]

is it actually true if the uniform spaces are not separated?

[Patrick Massot]

anyway, my wife calls me, so I'll give you my try. Note that the number of @ suggests I'm doing it wrong (looks like I'm fighting the interface):

import analysis.topology.topological_space
import analysis.topology.uniform_space

variables {X : Type*} (Y : set X) [u : uniform_space X]

lemma aux (f : filter X) : filter.vmap (λ  y : Y, y.val) f ≠ ⊥ ↔ f ⊓ filter.principal Y ≠ ⊥ :=
sorry

lemma rohan (h : @complete_space Y (uniform_space.vmap (λ  y : Y, y.val) u)) : is_closed Y :=
begin
  letI : uniform_space Y := (uniform_space.vmap (λ  y : Y, y.val) u),
  rw is_closed_iff_nhds,
  intros x ne_bot,
  have := @cauchy_vmap Y X _ _ (nhds x) (λ  y : Y, y.val) (le_refl _) cauchy_nhds,
  rw aux at this,
  specialize this ne_bot,
  rcases complete_space.complete this with ⟨x', H⟩,
  sorry
end

[Patrick Massot]

I this the aux lemma sounds plausible. The status in the main proof is:

x : X,
x' : ↥Y,
H : filter.vmap (λ (y : ↥Y), y.val) (nhds x) ≤ nhds x'
⊢ x ∈ Y

which looks promising, except maybe if things are not separated

[Reid Barton]

The book I looked at on uniform spaces had a lot of Hausdorff assumptions which were not always really required, but rather seemed to be used as a device to ward off evil spirits

[Kevin Buzzard]

So Rohan is a mathematics undergraduate and whilst this filter stuff might be a cool way to do it (and I know he's read my filter blog post), I think there is some merit in seeing a proof which is more what mathematics undergraduates are used to. So here are some dumb questions. Is the epsilon-delta definition of a sequence tending to a limit in Lean? I'm assuming the fact that open balls are open and that x is in the closure of Y iff Y intersects every open set containing x. Given all this, it seems to me to be completely feasible to prove the lemma "the way a mathematician proves it".

[Mario Carneiro]

There is an epsilon delta definition of continuity in a metric space, but I don't think we've unfolded the definition of a sequence limit

[Mario Carneiro]

The sequence limit is provided via the at_top filter on nat

[Kevin Buzzard]

@Rohan Mitta why not write down the mathematics proof you want to work in Lean and then see if you can get it to work. You might want to make some auxiliary definitions. I am still a bit unclear about whether the predicate "this sequence (i.e. function nat -> X) tends to this limit in the metric space X" is in Lean. I'm sure there will be some fancy filter version which works for second countable uniform semi-topologies or whatever, but the thing you're thinking about is a common notion in undergraduate mathematics and in my mind that is justifiction enough for it to be its own special predicate. I guess you could define it for topological spaces using open sets, and then prove that for metric spaces it's equivalent to the epsilon delta definition. This all sounds like very reasonable stuff to dump into an M2PM5 directory on the UROP repo (or the topology directory).

[Reid Barton]

I don't think we have the epsilon-N description of convergent sequences. For continuous functions we do have the epsilon-delta description, see continuous_of_metric and adjacent theorems.

[Patrick Massot]

We should definitely have this. I'll need it for teaching.

[Patrick Massot]

But it should be very easy to define

[Patrick Massot]

It's lunch time, so I can't golf the second half:

variables {α : Type*} [metric_space α]
open filter

example (u : ℕ → α) (a : α) : tendsto u at_top (nhds a) ↔
  ∀ ε > 0, ∃ (N : ℕ), ∀ {n}, n ≥ N → dist (u n) a < ε :=
⟨λ H ε εpos, mem_at_top_sets.1 $ mem_map.2 $ H (ball_mem_nhds _ εpos),
 λ H s s_nhd,
  begin
    rw [mem_map, mem_at_top_sets],
    rcases mem_nhds_iff_metric.1 s_nhd with ⟨ε, εpos, sub⟩,
    rcases H ε εpos with ⟨N, H⟩,
    existsi N,
    intros n nN,
    exact sub (mem_ball.2 $ H nN)
  end⟩

[Patrick Massot]

I'm returning to this thread because I think this should go into mathlib:

lemma seq_tendsto_iff (u : ℕ → α) (a : α) : tendsto u at_top (nhds a) ↔
  ∀ ε > 0, ∃ (N : ℕ), ∀ {n}, n ≥ N → dist (u n) a < ε :=
⟨λ H ε εpos, mem_at_top_sets.1 $ mem_map.2 $ H (ball_mem_nhds _ εpos),
 λ H s s_nhd, let ⟨ε, εpos, sub⟩ := mem_nhds_iff_metric.1 s_nhd in
   let ⟨N, H'⟩ := H ε εpos in mem_at_top_sets.2 ⟨N, λ n nN,
   sub $ mem_ball.2 $ H' nN⟩⟩

Mario, what do you think?

[Patrick Massot]

For teaching purposes, we could even define a new abbreviation like seq_tendsto u a for tendsto u at_top (nhds a) but maybe this kind of things does not belong to mathlib

[Mario Carneiro]

You can split that into two parts; first state it for an arbitrary filter and then reduce to the nhds filter

[Patrick Massot]

Too late: I turned it into term mode, so now it's read-only

[Patrick Massot]

It cannot be modified anymore

[Patrick Massot]

lemma tendsto_nhds_iff (u : β → α) (f : filter β) (a : α) : tendsto u f (nhds a) ↔
  ∀ ε > 0, ∃ s ∈ f.sets, ∀ {n}, n ∈ s → dist (u n) a < ε :=
⟨λ H ε εpos, ⟨u ⁻¹' ball a ε, ⟨H $ ball_mem_nhds a εpos, λ n h, h⟩⟩,
 λ H s s_nhd, let ⟨ε, εpos, sub⟩ := mem_nhds_iff_metric.1 s_nhd in
   let ⟨N, ⟨N_in, H'⟩⟩ := H ε εpos in f.sets_of_superset N_in (λ b b_in, sub $ H' b_in)⟩

[Patrick Massot]

Obfuscating is so fun

[Patrick Massot]

I understand how one could get addicted to it

[Mario Carneiro]

you missed a spot - ⟨N, ⟨N_in, H'⟩⟩ could be ⟨N, N_in, H'⟩

[Patrick Massot]

Oh you're right, the reader could infer from my version that N_in and H' go together

[Mario Carneiro]

By the way, if this proof was replaced with by finish I would argue it is even more obfuscatory

[Kevin Buzzard]

∀ ε > 0, ∃ (N : ℕ), ∀ {n}, n ≥ N → dist (u n) a < ε

Aah, it's just like the old days

[Patrick Massot]

The things we do for our students...

[Patrick Massot]

Mario, how would you call

lemma t [inhabited α] [semilattice_sup α] {p : α → Prop} :
(∃ (s : set α) (H : s ∈ (at_top : filter α).sets), ∀ n, n ∈ s → p n) ↔
(∃ N : α, ∀ n, n ≥ N → p n) :=

And do you have a one line long proof? It's meant to be a variation on mem_at_top_sets but deducing it is surprisingly painful here

[Patrick Massot]

My proof is

begin
  simp only [mem_at_top_sets, exists_prop],
  split ; intro h,
  { rcases h with ⟨s, ⟨⟨b, h⟩, h'⟩⟩,
    existsi b,
    intros n nb,
    exact h' _ (h n nb) },
  { rcases h with  ⟨N, h'⟩,
    existsi {a : α | a ≥ N },
    exact ⟨⟨N, λ _ x, x⟩, h'⟩ }
end

[Mario Carneiro]

I don't think there is a one line proof, although both conditions are equivalent to {n | p n} ∈ at_top.sets

[Mario Carneiro]

wait, isn't the proof rfl?

[Patrick Massot]

No

[Mario Carneiro]

I mean

lemma t [inhabited α] [semilattice_sup α] {p : α → Prop} :
  {n | p n} ∈ at_top.sets ↔ (∃ N : α, ∀ n, n ≥ N → p n) := iff.rfl

[Patrick Massot]

I need to go sleeping but @Rohan Mitta you can use https://gist.github.com/PatrickMassot/1b2d39011855ba43f3bf00c08051ad9e if you want to play with sequences in metric spaces. The lemma at bottom bridges the gap between what you see in lectures and mathlib context

[Mario Carneiro]

oh, this is just mem_at_top_sets

[Patrick Massot]

yes

[Patrick Massot]

the last bit you wrote is mem_at_top_sets

[Patrick Massot]

The question is: how to deduce my t lemma from this

[Mario Carneiro]

The fact (∃ (s : set α) (H : s ∈ F.sets), ∀ n, n ∈ s → p n) ↔ {n | p n} ∈ F.sets is true in any filter

[Mario Carneiro]

it's just saying that a filter is upward closed

[Mario Carneiro]

frankly I'd avoid it simply because the lhs is needlessly verbose

[Mario Carneiro]

just use upward_sets if it looks like the hypotheses of the lhs are about to appear

[Patrick Massot]

See the link above: the goal of this lemma is to allow the last proof to be so short

[Mario Carneiro]

I would state the previous theorem differently:

lemma tendsto_nhds_iff (u : β → α) (f : filter β) (a : α) : tendsto u f (nhds a) ↔
  ∀ ε > 0, {n | dist (u n) a < ε} ∈ f.sets := sorry

[Mario Carneiro]

this would be even nicer if we had a quantifier-like notation for {n | p n} ∈ f, but I can live with this

[Rohan Mitta]

Is this true? I can see how to go from an arbitrary sequence in a metric space to a filter, but don't see how it is possible in general to get from an arbitrary filter to a sequence.

import analysis.metric_space
import order.filter
noncomputable theory

lemma complete_iff_seq_complete {α : Type*} [metric_space α] :
  complete_space α ↔ ( ∀ (f : ℕ → α), cauchy (filter.map f at_top) → (∃ (a : α), tendsto f at_top (nhds a)) :=
begin
  split, intros H f Hf,
    exact (@complete_space.complete _ _ H _ Hf),
  sorry,
end

[Reid Barton]

You can get a sequence by for each n taking ε = 1/n and then applying the Cauchy property to the entourage of points at distance less than ε, and picking a point from the set you get out. cauchy_of_metric does some of this work for you

[Reid Barton]

I haven't checked but I expect this this defines a Cauchy sequence which you can then use to show the original filter converges.