Zulip Chat Archive

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.

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

true

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

It does!

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

And it's already in mathlib

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

Kevin Buzzard (Sep 26 2018 at 14:07):

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: Dec 20 2023 at 11:08 UTC