Zulip Chat Archive

Stream: Is there code for X?

Topic: product tends to zero


view this post on Zulip 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

view this post on Zulip Adam Topaz (Apr 05 2021 at 15:33):

docs#tendsto_mul might help?

view this post on Zulip Adam Topaz (Apr 05 2021 at 15:34):

Or docs#filter.tendsto.mul

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Apr 05 2021 at 15:35):

(deleted)

view this post on Zulip Adam Topaz (Apr 05 2021 at 15:36):

docs#filter.tendsto.const_mul

view this post on Zulip Adam Topaz (Apr 05 2021 at 15:37):

Or mul_const in this case?

view this post on Zulip Bhavik Mehta (Apr 05 2021 at 15:37):

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

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 15:42):

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

view this post on Zulip Adam Topaz (Apr 05 2021 at 15:44):

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

view this post on Zulip 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!

view this post on Zulip Yakov Pechersky (Apr 05 2021 at 16:03):

docs#filter.tendsto.inv' ?

view this post on Zulip Yakov Pechersky (Apr 05 2021 at 16:03):

Although maybe doesn't work here due to noncontinuous inv

view this post on Zulip Bhavik Mehta (Apr 05 2021 at 16:04):

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

view this post on Zulip Adam Topaz (Apr 05 2021 at 16:06):

docs#filter.tendsto.inv_tendsto_zero

view this post on Zulip Adam Topaz (Apr 05 2021 at 16:07):

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

view this post on Zulip Bhavik Mehta (Apr 05 2021 at 16:08):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Apr 05 2021 at 16:25):

Are there lemmas about tendsto and order preserving maps?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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