## Stream: Is there code for X?

### Topic: product tends to zero

#### Bhavik Mehta (Apr 05 2021 at 15:31):

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 (Apr 05 2021 at 15:33):

docs#tendsto_mul might help?

#### Bhavik Mehta (Apr 05 2021 at 15:35):

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

(deleted)

#### Adam Topaz (Apr 05 2021 at 15:36):

docs#filter.tendsto.const_mul

#### Adam Topaz (Apr 05 2021 at 15:37):

Or mul_const in this case?

#### Bhavik Mehta (Apr 05 2021 at 15:37):

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

#### Kevin Buzzard (Apr 05 2021 at 15:42):

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

#### Adam Topaz (Apr 05 2021 at 15:44):

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

#### Bhavik Mehta (Apr 05 2021 at 16:00):

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 (Apr 05 2021 at 16:03):

Although maybe doesn't work here due to noncontinuous inv

#### Bhavik Mehta (Apr 05 2021 at 16:04):

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

#### Adam Topaz (Apr 05 2021 at 16:06):

docs#filter.tendsto.inv_tendsto_zero

#### Adam Topaz (Apr 05 2021 at 16:07):

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

#### Bhavik Mehta (Apr 05 2021 at 16:08):

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

#### Bhavik Mehta (Apr 05 2021 at 16:20):

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 (Apr 05 2021 at 16:25):

Are there lemmas about tendsto and order preserving maps?

#### Bhavik Mehta (Apr 05 2021 at 16:26):

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

#### Bhavik Mehta (Apr 05 2021 at 16:29):

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 (Apr 05 2021 at 16:51):

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

Last updated: May 17 2021 at 16:26 UTC