expressing limits and continuity

Stream: new members

[Jason Orendorff]

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]

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

[Jason Orendorff]

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]

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

[Patrick Massot]

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]

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

[Jason Orendorff]

I didn't know that.

[Kevin Buzzard]

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

[Patrick Massot]

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

[Jason Orendorff]

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

[Patrick Massot]

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]

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

[Jason Orendorff]

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]

it's really impressive

[Jason Orendorff]

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]

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]

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

[Jason Orendorff]

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]

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"

[Jason Orendorff]

Yes, I know about it