f = o(g) as a filter

Stream: maths

[Yury G. Kudryashov]

#xy: I want to have $\Re z \to +\infty$, $\Im z =o((\Re z)^2)$ as a filter. Clearly, it's comap re atTop ⊓ l for some l. To define l, I have two choices:

• define Filter.isLittleO : Filter (ℝ × ℝ) as ⨅ c > 0, 𝓟 {(x, y) | abs x ≤ c * abs y} and take comap under $f(z)=((\Re z)^2, \Im z)$ or $f(z)=(\Re z, \sqrt{|\Im z|})$;
• define Filter.isLittleO (f : α → E) (g : α → F) : Filter α as ⨅ c > 0, 𝓟 {(x, y) | ‖f x‖ ≤ c * ‖g y‖}

With the first approach, I get 1 filter (and use comap if needed). With the second approach, I get a family of filters indexed by α, f, and g. What would you recommend?

[Yaël Dillies]

I would tend towards the second option for usability, but I'm not sure how strong that argument is

[Antoine Chambert-Loir]

I would tend to something like the first one, but would consider 1) having it for topological fields or rings, 2) removing absolute values, 3) passing through a o(1) filter if possible.

[Yury G. Kudryashov]

What exactly do you suggest?

[Antoine Chambert-Loir]

Comap the o(1) by Im(z)/Re(z²), for example

[Yury G. Kudryashov]

I want to avoid division.

[Yury G. Kudryashov]

Otherwise I would comap nhds 0

[Yury G. Kudryashov]

OTOH, I can do exactly this for my goal, and postpone adding a more general definition until someone needs it.

[Yury G. Kudryashov]

I mean, define the filter as comap (fun z => im z / (re z) ^ 2) (nhds 0). Since I have re z -> ∞ anyway, it doesn't make any difference.