Zulip Chat Archive

Stream: maths

Topic: Continuous Functions Preserve Limits


view this post on Zulip 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

view this post on Zulip Johannes Hölzl (Sep 26 2018 at 12:53):

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

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 12:53):

he's just editing :-)

view this post on Zulip Rohan Mitta (Sep 26 2018 at 12:53):

Sorry I've just updated it with continuous f

view this post on Zulip Johannes Hölzl (Sep 26 2018 at 12:54):

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

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 12:54):

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

view this post on Zulip 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]

view this post on Zulip Johannes Hölzl (Sep 26 2018 at 12:56):

hehe, peer proving

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 12:57):

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

view this post on Zulip 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.

view this post on Zulip Rohan Mitta (Sep 26 2018 at 13:00):

Brilliant, that worked!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 13:11):

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

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 13:11):

We're so close :-)

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 13:12):

Do I have to actually unravel things here?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:19):

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

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:20):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 26 2018 at 13:23):

try constructor

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:23):

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

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:24):

Kenny, this works but it's even more ridiculous

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:25):

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

view this post on Zulip Rob Lewis (Sep 26 2018 at 13:25):

linarith should work too.

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:25):

true

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:26):

It does!

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:26):

And it's already in mathlib

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:26):

Do we have the contraction mapping theorem then?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 26 2018 at 13:34):

Now you can try to break it into ten lemmas

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 14:06):

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

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 14:07):

He's pushed!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Rohan Mitta (Sep 26 2018 at 15:30):

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

view this post on Zulip Patrick Massot (Sep 26 2018 at 15:49):

Congratulations Rohan!


Last updated: May 19 2021 at 00:40 UTC