Zulip Chat Archive

Stream: new members

Topic: expressing limits and continuity


view this post on Zulip Jason Orendorff (Jul 03 2020 at 18:21):

I'm trying to prove

lemma lim_mul {seq :   } {l : } (a : )
: filter.tendsto (λ x, seq x) filter.at_top (nhds l) 
  filter.tendsto (λ x, a * seq x) filter.at_top (nhds (a * l))

Is filter.tendsto.comp the easiest way to approach it? To me, informally, this follows from * being continuous, but I don't know how to tell Lean that.

view this post on Zulip Jason Orendorff (Jul 03 2020 at 18:44):

Oh, the definition of continuous_at is almost exactly what's left after applying filter.tendsto.comp...

view this post on Zulip Jason Orendorff (Jul 03 2020 at 18:52):

this proof ends up being absurdly nice

lemma lim_mul {seq :   } {l : } (a : )
: filter.tendsto (λ x, seq x) filter.at_top (nhds l) 
  filter.tendsto (λ x, a * seq x) filter.at_top (nhds (a * l))
:= by {
  intro h₀,
  rw (show (λ x, a * seq x) = (λ b, a * b)  seq, by refl),
  refine filter.tendsto.comp _ h₀,
  apply continuous.continuous_at,
  apply uniform_continuous.continuous _,
  apply real.uniform_continuous_mul_const,
}

view this post on Zulip Patrick Massot (Jul 03 2020 at 18:59):

Without context it's hard to help you. What do you want to use and what do you want to redo?

view this post on Zulip Patrick Massot (Jul 03 2020 at 19:00):

Maybe the preliminary question is even: do you know that what you stated can be proved by

lemma lim_mul {seq :   } {l : } (a : )
: filter.tendsto (λ x, seq x) filter.at_top (nhds l) 
  filter.tendsto (λ x, a * seq x) filter.at_top (nhds (a * l)) :=
tendsto_const_nhds.mul

view this post on Zulip Patrick Massot (Jul 03 2020 at 19:01):

If yes, then I return to the previous question: what do you want to assume in your proof?

view this post on Zulip Jason Orendorff (Jul 03 2020 at 19:12):

I didn't know that.

view this post on Zulip Kevin Buzzard (Jul 03 2020 at 19:29):

Filters are super powerful. Patrick just wrote your informal proof in one line

view this post on Zulip Patrick Massot (Jul 03 2020 at 19:31):

No, his informal proof uses internal details of the special case he is working on.

view this post on Zulip Jason Orendorff (Jul 03 2020 at 19:40):

It's impressive. I forgot to look for a structure that has the exact property I want (continuity of (*))

view this post on Zulip Patrick Massot (Jul 03 2020 at 19:40):

Jason, just to make sure you can follow the compressed notation: my proof combines https://leanprover-community.github.io/mathlib_docs/topology/algebra/monoid.html#tendsto_mul and https://leanprover-community.github.io/mathlib_docs/topology/basic.html#tendsto_const_nhds

view this post on Zulip Patrick Massot (Jul 03 2020 at 19:41):

Don't hesitate to ask if the syntax used for this combination or how elaboration takes place is mysterious

view this post on Zulip Jason Orendorff (Jul 03 2020 at 19:48):

thanks! i did figure that part out, I um ... it is actually the math that I don't know :embarrassed: but i see that filter.tendsto.mulis one of a big toolkit of lemmas for proving a function is continuous at a point; the structure of your proof can mimic the structure of the function

view this post on Zulip Jason Orendorff (Jul 03 2020 at 19:51):

it's really impressive

view this post on Zulip Jason Orendorff (Jul 03 2020 at 19:53):

Patrick Massot said:

No, his informal proof uses internal details of the special case he is working on.

I think Kevin meant "To me, informally, this follows from * being continuous" not my Lean proof

view this post on Zulip Reid Barton (Jul 03 2020 at 19:53):

If your end goal is to prove continuity of some function then you probably don't need to drop down to the level of filters (unless you're defining the function "from scratch" perhaps).

view this post on Zulip Jason Orendorff (Jul 03 2020 at 19:53):

Right, it just so happened I had to plug it into something that wanted a tendsto

view this post on Zulip Jason Orendorff (Jul 03 2020 at 19:54):

I'm at the stage where Lean drives me around by asking for things, I really don't know enough of the library to design properly

view this post on Zulip Patrick Massot (Jul 03 2020 at 19:56):

About the compressed syntax, are you familiar with https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html, the paragraph starting with "The dot notation is convenient"

view this post on Zulip Jason Orendorff (Jul 03 2020 at 19:59):

Yes, I know about it


Last updated: May 12 2021 at 23:13 UTC