Continuous Functions Preserve Limits

Stream: maths

[Rohan Mitta]

Is this in mathlib (or anything like this)?

import analysis.metric_space
import order.filter
example {X : Type*} {Y : Type*} [metric_space X] [metric_space Y] (f : X → Y) (H1 : continuous f) (seq : ℕ → X)
  (a : X) (H : filter.tendsto seq filter.at_top (nhds a)) : filter.tendsto (f ∘ seq) filter.at_top (nhds (f a))
  := sorry

[Johannes Hölzl]

this doesn't hold. f needs to be continuous at a

[Kevin Buzzard]

he's just editing :-)

[Rohan Mitta]

Sorry I've just updated it with continuous f

[Johannes Hölzl]

otherwise it is composition of continuous.tendsto, tendsto.comp and H

[Kevin Buzzard]

Thanks again Johannes. I've never used this stuff before.

[Kevin Buzzard]

so all I do is offer encouragement and tell Rohan to ask his questions here :-) [he's sitting next to me]

[Johannes Hölzl]

hehe, peer proving

[Johannes Hölzl]

But this lemma is the reason why we use filters. We can express a lot of things as filters, and then just compose them

[Kevin Buzzard]

I encourage Rohan to formalise precisely the statement he needs and ask it here. I think that's a good way of learning how to think about Lean.

[Kevin Buzzard]

He's almost proved the contraction mapping theorem, this is just the last bit.

[Kevin Buzzard]

I could see it was going to follow from standard filter stuff, I just don't yet know how to drive filters. I am all over the road.

[Rohan Mitta]

Brilliant, that worked!

[Patrick Massot]

For those reading without typing: the proof that Rohan wanted is tendsto.comp H (H1.tendsto a) This is the point of filters: the limit lemmas don't care whether you take the limit of a sequence at infinity, the limit of a function at a point or whatever

[Patrick Massot]

Extra tip for Rohan: f, seq and a can be implicit arguments, they can be inferred from H and H1 by unification

[Patrick Massot]

a last one: your assumptions that X and Y are metric spaces are useless. You can replace them by topological_space without changing anything else

[Patrick Massot]

Note also that the proof is much shorter than the statement, and very easy to remember, so the final tip may be to erase the lemma...

[Kevin Buzzard]

tendsto (λ (n : ℕ), n + 1) at_top at_top

[Kevin Buzzard]

We're so close :-)

[Kevin Buzzard]

Do I have to actually unravel things here?

[Patrick Massot]

I did the beginning up to the point where I hate those things:

example : tendsto (λ (n : ℕ), n + 1) at_top at_top :=
begin
  intros s s_in,
  rw mem_at_top_sets at s_in,
  cases s_in with a h,
  rw [mem_map, mem_at_top_sets],
  existsi a,
  intros b H,
  change b+1 ∈ s,
  apply h,
  sorry
end

[Patrick Massot]

State is now b ≥ a ⊢ b + 1 ≥ a

[Patrick Massot]

Of course the change in the middle is purely psychological, you can remove it

[Patrick Massot]

Full proof is

example : tendsto (λ (n : ℕ), n + 1) at_top at_top :=
begin
  intros s s_in,
  rw mem_at_top_sets at s_in,
  cases s_in with a h,
  rw [mem_map, mem_at_top_sets],
  existsi a,
  intros b H,
  exact h _ (le_trans H (nat.le_succ b))
end

[Kenny Lau]

try constructor

[Patrick Massot]

@Simon Hudon I guess this is yet another test for mono

[Patrick Massot]

Kenny, this works but it's even more ridiculous

[Patrick Massot]

The only acceptable answer here is a finishing tactic (mono should do the trick)

[Rob Lewis]

linarith should work too.

[Patrick Massot]

true

[Patrick Massot]

It does!

[Patrick Massot]

And it's already in mathlib

[Patrick Massot]

Do we have the contraction mapping theorem then?

[Patrick Massot]

That being said, this proof is still too handcrafted. We should prove a lemma saying that the identity of a linearly_ordered type goes to top at top, and then use a version of squeeze

[Rohan Mitta]

I've just finished a very long proof of

theorem Banach_fixed_point {α : Type*} [metric_space α] [complete_space α] (H1 : nonempty α) {f : α → α} (H : is_contraction f)
: ∃! (p : α), f p = p := sorry

[Patrick Massot]

Now you can try to break it into ten lemmas

[Patrick Massot]

I need to go and do real work, but I'll be happy to read your proof once it's available

[Kenny Lau]

import order.filter

open filter

example : tendsto (λ (n : ℕ), n + 1) at_top at_top :=
begin
  intros s,
  rw [mem_at_top_sets, mem_map_sets_iff],
  rintro ⟨N, h1⟩,
  refine ⟨{b | b ≥ N}, mem_at_top_sets.2 ⟨_, λ _, id⟩, _⟩,
  rintro n ⟨k, h2, h3⟩, subst h3,
  apply h1,
  constructor,
  exact h2
end

[Kevin Buzzard]

example (X : Type*) (f : ℕ → X) (F : filter X) (H : tendsto f at_top F) :
tendsto (λ n, f (n + 1)) at_top F :=
tendsto.comp (tendsto_def.2 $ λ U HU,
  let ⟨a,Ha⟩ := mem_at_top_sets.1 HU in
  mem_at_top_sets.2 ⟨a,λ x Hx,Ha _ $ le_trans Hx $ by simp⟩) H

[Kevin Buzzard]

example : tendsto (λ (n : ℕ), n + 1) at_top at_top :=
tendsto_def.2 $ λ U HU,
  let ⟨a,Ha⟩ := mem_at_top_sets.1 HU in
  mem_at_top_sets.2 ⟨a,λ x Hx,Ha _ $ le_trans Hx $ by simp⟩

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/Topology/Material/banach_contraction.lean

[Kevin Buzzard]

He's pushed!

[Kevin Buzzard]

rofl he has the vmap version of filter so it doesn't compile for me :-) I'll fix it. @Rohan Mitta I'm editing your file so that it compiles with the most recent mathlib

[Kevin Buzzard]

rofl there's still a sorry! Rohan I think you hadn't saved before you pushed :-) OK so the current state of the contraction mapping theorem is that the only finished version is on a laptop owned by an undergraduate who has just gone off to prepare a treasure hunt for Fresher's week.

[Rohan Mitta]

Okay whoops, I've saved and pushed again. Hopefully its all there now?

[Patrick Massot]

Congratulations Rohan!