## Stream: maths

### Topic: Continuous Functions Preserve Limits

#### Rohan Mitta (Sep 26 2018 at 12:52):

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 (Sep 26 2018 at 12:53):

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

#### Kevin Buzzard (Sep 26 2018 at 12:53):

he's just editing :-)

#### Rohan Mitta (Sep 26 2018 at 12:53):

Sorry I've just updated it with continuous f

#### Johannes Hölzl (Sep 26 2018 at 12:54):

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

#### Kevin Buzzard (Sep 26 2018 at 12:54):

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

#### Kevin Buzzard (Sep 26 2018 at 12:54):

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

#### Johannes Hölzl (Sep 26 2018 at 12:56):

hehe, peer proving

#### Johannes Hölzl (Sep 26 2018 at 12:56):

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 (Sep 26 2018 at 12:57):

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 (Sep 26 2018 at 12:57):

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

#### Kevin Buzzard (Sep 26 2018 at 12:58):

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 (Sep 26 2018 at 13:00):

Brilliant, that worked!

#### Patrick Massot (Sep 26 2018 at 13:05):

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 (Sep 26 2018 at 13:07):

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

#### Patrick Massot (Sep 26 2018 at 13:09):

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 (Sep 26 2018 at 13:11):

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 (Sep 26 2018 at 13:11):

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

#### Kevin Buzzard (Sep 26 2018 at 13:11):

We're so close :-)

#### Kevin Buzzard (Sep 26 2018 at 13:12):

Do I have to actually unravel things here?

#### Patrick Massot (Sep 26 2018 at 13:19):

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 (Sep 26 2018 at 13:19):

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

#### Patrick Massot (Sep 26 2018 at 13:20):

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

#### Patrick Massot (Sep 26 2018 at 13:23):

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 (Sep 26 2018 at 13:23):

try constructor

#### Patrick Massot (Sep 26 2018 at 13:23):

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

#### Patrick Massot (Sep 26 2018 at 13:24):

Kenny, this works but it's even more ridiculous

#### Patrick Massot (Sep 26 2018 at 13:25):

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

#### Rob Lewis (Sep 26 2018 at 13:25):

linarith should work too.

true

It does!

#### Patrick Massot (Sep 26 2018 at 13:26):

Do we have the contraction mapping theorem then?

#### Patrick Massot (Sep 26 2018 at 13:28):

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 (Sep 26 2018 at 13:32):

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 (Sep 26 2018 at 13:34):

Now you can try to break it into ten lemmas

#### Patrick Massot (Sep 26 2018 at 13:37):

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

#### Kenny Lau (Sep 26 2018 at 13:42):

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 (Sep 26 2018 at 13:54):

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 (Sep 26 2018 at 13:55): 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 (Sep 26 2018 at 14:06):

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

He's pushed!

#### Kevin Buzzard (Sep 26 2018 at 14:08):

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 (Sep 26 2018 at 14:10):

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 (Sep 26 2018 at 15:30):

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

#### Patrick Massot (Sep 26 2018 at 15:49):

Congratulations Rohan!

Last updated: May 19 2021 at 00:40 UTC