Zulip Chat Archive

Stream: maths

Topic: tendsto at_top at_top


view this post on Zulip Chris Hughes (Nov 29 2018 at 23:11):

I'm trying to work out how filters work. Is the following true/easy to prove. Which is the better way to state that a function goes to infinity.

import data.complex.basic order.filter

open filter

instance : preorder  :=
{ le := λ x y, x.abs  y.abs,
  le_refl := λ x, le_refl x.abs,
  le_trans := λ x y z, @le_trans  _ _ _ _ }

example (f :   ) : tendsto f at_top at_top 
   x : ,  r,  z : , r < z.abs  x < (f z).abs

view this post on Zulip Chris Hughes (Nov 30 2018 at 01:22):

Okay. I managed to prove this. My first experience dealing with filters.

lemma tendsto_at_top_at_top_iff {α β : Type} [preorder α] [preorder β]
  [ : nonempty α]
  (h : directed (@has_le.le α _) id)
  (f : α  β) :
  tendsto f at_top at_top   (b : β),  (i : α),  (a : α), i  a  b  f a :=
have directed ge (λ (a : α), principal {b : α | a  b}),
  from λ a b, let z, hz := h b a in
    z, λ s h x hzx, h (le_trans hz.2 hzx),
      λ s h x hzx, h (le_trans hz.1 hzx),
by rw [tendsto_at_top, at_top, infi_sets_eq this ]; simp

view this post on Zulip Chris Hughes (Nov 30 2018 at 01:27):

Is there a better way of stating directed has_le.le id?

view this post on Zulip Mario Carneiro (Nov 30 2018 at 03:18):

I don't think so; there are directed sets and directed images but directed types haven't come up. Using directed (<=) (@id a) should work fine

view this post on Zulip Sebastien Gouezel (Nov 30 2018 at 07:14):

If you want to define convergence to infinity in C, or another metric space, it looks strange to introduce an artificial order. It would probably be more natural to introduce a filter at_infinity, generated by the complements of closed balls with arbitrary center and radius. Another good exercise with filters :) Even better, show that this filter is trivial if and only if the space is bounded (but you will need #PR464 for the notion of boundedness in a metric space)

view this post on Zulip Mario Carneiro (Nov 30 2018 at 07:28):

I guess that the usual filter here is the one used in the alexandroff one point compactification - the complements of compact sets

view this post on Zulip Patrick Massot (Nov 30 2018 at 07:29):

I agree the order thing looks very artificial

view this post on Zulip Patrick Massot (Nov 30 2018 at 07:31):

We could go straight to https://en.wikipedia.org/wiki/End_(topology) but I guess that the infinity filter in a normed real vector space is a better first target

view this post on Zulip Sebastien Gouezel (Nov 30 2018 at 07:45):

You really have two natural filters, which do not coincide in general (but do coincide in proper spaces): the complements of compact sets, and the complements of bounded sets. I have had more use in my own research for the second one, but both are definitely relevant.

view this post on Zulip Kevin Buzzard (Nov 30 2018 at 07:45):

I guess the preorder looks strange to mathematicians because on the whole they don't usually deal with the concept of a preorder, like semirings look strange. Chris is taking a metric space and a point, and looking at the "distance to that point" real-valued function; and any function from any space to the reals gives a pre-order structure on the the space because in contrast to partial offers you can just pull back a preorder along an arbitrary map. Why this doesn't come up more often I don't know, but I agree that it looks strange.

view this post on Zulip Sebastien Gouezel (Nov 30 2018 at 07:47):

One problem with this order thing is that it depends on the choice of a basepoint, while this can be avoided with the more usual approaches.


Last updated: May 19 2021 at 00:40 UTC