## Stream: maths

### Topic: tendsto at_top at_top

#### 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


#### 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 β]
[hα : 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 hα]; simp


#### Chris Hughes (Nov 30 2018 at 01:27):

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

#### 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

#### 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)

#### 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

#### Patrick Massot (Nov 30 2018 at 07:29):

I agree the order thing looks very artificial

#### 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

#### 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.

#### 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.

#### 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