IsLittleO as Tendsto

Stream: mathlib4

[Yury G. Kudryashov]

In a project I'm working on, I need the following filter:

def myFilter : Filter ℂ := ⨅ (c : ℝ) (_ : 0 < c), 𝓟 {z | |z.im| ≤ c * z.re ^ 2}

lemma tendsto_myFilter {α} {f : α → ℂ} {l} :
    Tendsto f l myFilter ↔ (fun x ↦ (f x).im) =o[l] (fun x ↦ (f x).re ^ 2) := sorry

[Yury G. Kudryashov]

I think about addint a more general version to Mathlib. E.g.,

def Filter.littleO (f : α → E) (g : α → F) : Filter α := ⨅ (c : ℝ) (_ : 0 < c), 𝓟 {x | ‖f x‖ ≤ c * ‖g x‖}

[Yury G. Kudryashov]

Is there a better approach?