∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E},
  b < a → (f =O[Filter.atTop] fun x => x ^ (-a)) → (fun t => Real.log t • f t) =O[Filter.atTop] fun x => x ^ (-b)