tendsto at_top at_top

Stream: maths

[Chris Hughes]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Patrick Massot]

I agree the order thing looks very artificial

[Patrick Massot]

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]

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]

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]

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.