α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * f a)) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * g a)) l (𝓝 0)
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : SuperpolynomialDecay l k f
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ SuperpolynomialDecay l k g
rw [superpolynomialDecay_iff_abs_tendsto_zero] at hf⊢
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * f a)) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ abs (k x ^ z * g x) ≤ abs (k x ^ z * f x)
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * f a)) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * g a)) l (𝓝 0)
refine' fun z =>
  tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hf z)
    (eventually_of_forall fun x => abs_nonneg _) (hfg.mono fun x hx => _)
no goals
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * f a)) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ abs (k x ^ z * g x) ≤ abs (k x ^ z * f x)
calc
  |k x ^ z * g x| = |k x ^ z| * |g x| := abs_mul (k x ^ z) (g x)
  _ ≤ |k x ^ z| * |f x| := by gcongr; exact hx
  _ = |k x ^ z * f x| := (abs_mul (k x ^ z) (f x)).symm
case h
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * f a)) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ abs (g x) ≤ abs (f x)
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * f a)) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ abs (k x ^ z) * abs (g x) ≤ abs (k x ^ z) * abs (f x)
gcongr
no goals
case h
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * f a)) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ abs (g x) ≤ abs (f x)
exact hx