α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
⊢ f =o[l] fun a => k a ^ z
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =o[l] fun a => k a ^ z
refine' ⟨fun h z => _, fun h => (superpolynomialDecay_iff_isBigO f hk).2 fun z => (h z).isBigO⟩
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ f =o[l] fun a => k a ^ z
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
⊢ f =o[l] fun a => k a ^ z
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : (fun x => 1) =o[l] k
⊢ f =o[l] fun a => k a ^ z
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ f =o[l] fun a => k a ^ z
have : (fun _ : α => (1 : β)) =o[l] k :=
  isLittleO_of_tendsto' (hk0.mono fun x hkx hkx' => absurd hkx' hkx)
    (by simpa using hk.inv_tendsto_atTop)
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this✝ : (fun x => 1) =o[l] k
this : f =o[l] fun x => k x * k x ^ (z - 1)
⊢ f =o[l] fun a => k a ^ z
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : (fun x => 1) =o[l] k
⊢ f =o[l] fun a => k a ^ z
have : f =o[l] fun x : α => k x * k x ^ (z - 1) := by
  simpa using this.mul_isBigO ((superpolynomialDecay_iff_isBigO f hk).1 h <| z - 1)
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this✝ : (fun x => 1) =o[l] k
this : f =o[l] fun x => k x * k x ^ (z - 1)
x : α
hkx : k x ≠ 0
⊢ ‖k x * k x ^ (z - 1)‖ = 1 * ‖k x ^ z‖
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this✝ : (fun x => 1) =o[l] k
this : f =o[l] fun x => k x * k x ^ (z - 1)
⊢ f =o[l] fun a => k a ^ z
refine' this.trans_isBigO (IsBigO.of_bound 1 (hk0.mono fun x hkx => le_of_eq _))
no goals
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this✝ : (fun x => 1) =o[l] k
this : f =o[l] fun x => k x * k x ^ (z - 1)
x : α
hkx : k x ≠ 0
⊢ ‖k x * k x ^ (z - 1)‖ = 1 * ‖k x ^ z‖
rw [one_mul, zpow_sub_one₀ hkx, mul_comm (k x), mul_assoc, inv_mul_cancel hkx, mul_one]
no goals
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ Tendsto (fun x => 1 / k x) l (𝓝 0)
simpa using hk.inv_tendsto_atTop
no goals
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : (fun x => 1) =o[l] k
⊢ f =o[l] fun x => k x * k x ^ (z - 1)
simpa using this.mul_isBigO ((superpolynomialDecay_iff_isBigO f hk).1 h <| z - 1)