product tends to zero

Stream: Is there code for X?

[Bhavik Mehta]

I presume I'm just missing an import here, but library_search and suggest weren't helpful, how about zulip?

import topology.instances.real

open filter

example (i : ℕ → ℝ) (θ : ℝ) (hi : tendsto i at_top (nhds 0)) :
  tendsto (λ x, i x * θ) at_top (nhds 0) :=
begin
  sorry
end

[Adam Topaz]

docs#tendsto_mul might help?

[Adam Topaz]

Or docs#filter.tendsto.mul

[Bhavik Mehta]

I had a go at that and it gives this error:

invalid apply tactic, failed to unify
  tendsto (λ (x : ℕ), i x * θ) at_top (nhds 0)
with
  tendsto (λ (p : ?m_1 × ?m_1), p.fst * p.snd) (nhds (?m_4, ?m_5)) (nhds (?m_4 * ?m_5))

I think it's intended for product filters

[Bhavik Mehta]

(deleted)

[Adam Topaz]

docs#filter.tendsto.const_mul

[Adam Topaz]

Or mul_const in this case?

[Bhavik Mehta]

Yup, by simpa using tendsto.mul_const θ hi does it. Thanks!

[Kevin Buzzard]

I love that the description of this stream is "human powered library search" :-)

[Adam Topaz]

I bet gpt would have found a proof for this :wink:

[Bhavik Mehta]

import topology.instances.real
import topology.sequences
import topology.algebra.group_with_zero

open filter

example (f : ℕ → ℝ) (hf : tendsto f at_top at_top) :
  tendsto (λ x, (f x)⁻¹) at_top (nhds 0) :=
begin

end

Round two!

[Yakov Pechersky]

docs#filter.tendsto.inv' ?

[Yakov Pechersky]

Although maybe doesn't work here due to noncontinuous inv

[Bhavik Mehta]

Doesn't work here because the hypothesis target filter isn't a neighbourhood

[Adam Topaz]

docs#filter.tendsto.inv_tendsto_zero

[Adam Topaz]

I didn't actually look at it but the name sounds useful :wink:

[Bhavik Mehta]

That one doesn't work but the one immediately before it does! :D

[Bhavik Mehta]

And finally, what's the nicer proof of:

example : tendsto (λ (i : ℕ), (i : ℝ)) at_top at_top :=
tendsto_at_top_at_top_of_monotone (λ x y, nat.cast_le.2) (λ x, ⟨nat_ceil x, le_nat_ceil x⟩)

My proof works but it's hard to believe that there's nothing cleaner

[Yakov Pechersky]

Are there lemmas about tendsto and order preserving maps?

[Bhavik Mehta]

The best I could find were docs#filter.tendsto_at_top_at_top_of_monotone and things around that

[Bhavik Mehta]

Ooh actually I just found docs#tendsto_one_div_add_at_top_nhds_0_nat which comes a lot closer to my original problem without needing to break it into bits

[Bhavik Mehta]

And docs#tendsto_coe_nat_at_top_at_top is the exact example I was expecting to see earlier