Stream: new members

Topic: expressing limits and continuity

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.

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...

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,
}


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?

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


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?

Jason Orendorff (Jul 03 2020 at 19:12):

I didn't know that.

Kevin Buzzard (Jul 03 2020 at 19:29):

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

Patrick Massot (Jul 03 2020 at 19:31):

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

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 (*))

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

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

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

Jason Orendorff (Jul 03 2020 at 19:51):

it's really impressive

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

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).

Jason Orendorff (Jul 03 2020 at 19:53):

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

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

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"