combining filters

Stream: Is there code for X?

[Alex Kontorovich]

Can someone please remind me what the tactic is for rewriting inside filters? E.g.:

import Mathlib

open Topology

example {f g h : ℝ → ℝ} {x : ℝ} (hfg : ∀ᶠ (y : ℝ) in 𝓝 x, f y = g y) (hgh : g =o[𝓝 x] h) :
  f =o[𝓝 x] h := by sorry

Thanks!

[David Loeffler]

I'm not sure there's a tactic, per se, but there's a lemma IsLittleO.congr' showing that you can exchange either side of a little-O statement with something eventually equal. Here's a one-liner:

example {f g h : ℝ → ℝ} {x : ℝ} (hfg : ∀ᶠ (y : ℝ) in 𝓝 x, f y = g y) (hgh : g =o[𝓝 x] h) :
    f =o[𝓝 x] h := hgh.congr' (hfg.mp (eventually_of_forall (fun x hx ↦ hx.symm))) (by rfl)

[Alex Kontorovich]

Perfect, thanks!

[Yury G. Kudryashov]

See also docs#Filter.EventuallyEq.trans_isLittleO

[Yury G. Kudryashov]

And you can use it with calc like

calc
  f =ᶠ[𝓝 x] g := hfg
  _ =o[𝓝 x] h := hgh