[GOAL]
α : Type u_1
β : Type u_2
l✝ : Filter α
k✝ f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto (fun a => k a ^ z * OfNat.ofNat 0 a) l (𝓝 0)
[PROOFSTEP]
simpa only [Pi.zero_apply, mul_zero] using tendsto_const_nhds
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousAdd β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (f + g) a) l (𝓝 0)
[PROOFSTEP]
simpa only [mul_add, add_zero, Pi.add_apply] using (hf z).add (hg z)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (f * g) a) l (𝓝 0)
[PROOFSTEP]
simpa only [mul_assoc, one_mul, mul_zero, pow_zero] using (hf z).mul (hg 0)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
c : β
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (fun n => f n * c) a) l (𝓝 0)
[PROOFSTEP]
simpa only [← mul_assoc, zero_mul] using Tendsto.mul_const c (hf z)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
z : ℕ
s : Set β
hs : IsOpen s
hs0 : 0 ∈ s
x : α
hx : x ∈ (fun a => k a ^ (z + 1) * f a) ⁻¹' s
⊢ x ∈ (fun a => k a ^ z * (k * f) a) ⁻¹' s
[PROOFSTEP]
simpa only [Set.mem_preimage, Pi.mul_apply, ← mul_assoc, ← pow_succ'] using hx
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f)
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ Nat.zero * f)
[PROOFSTEP]
simpa only [Nat.zero_eq, one_mul, pow_zero] using hf
[GOAL]
case succ
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f)
⊢ SuperpolynomialDecay l k (k ^ Nat.succ n * f)
[PROOFSTEP]
simpa only [pow_succ, mul_assoc] using hn.param_mul
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝³ : TopologicalSpace β
inst✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p✝ p q : β[X]
hp : SuperpolynomialDecay l k fun x => eval (k x) p * f x
hq : SuperpolynomialDecay l k fun x => eval (k x) q * f x
⊢ SuperpolynomialDecay l k fun x => eval (k x) (p + q) * f x
[PROOFSTEP]
simpa [add_mul] using hp.add hq
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝³ : TopologicalSpace β
inst✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p : β[X]
n : ℕ
c : β
⊢ SuperpolynomialDecay l k fun x => eval (k x) (↑(monomial n) c) * f x
[PROOFSTEP]
simpa [mul_assoc] using (hf.param_pow_mul n).const_mul c
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
⊢ (∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a => |k a|) fun a => |f a|
[PROOFSTEP]
simp_rw [SuperpolynomialDecay, abs_mul, abs_pow]
[GOAL]
α : 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
[PROOFSTEP]
rw [superpolynomialDecay_iff_abs_tendsto_zero] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * g a|) l (𝓝 0)
[PROOFSTEP]
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 => _)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z * g x| ≤ |k x ^ z * f x|
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z| * |g x| ≤ |k x ^ z| * |f x|
[PROOFSTEP]
gcongr
[GOAL]
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 => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |g x| ≤ |f x|
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Field β
inst✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n => f n * c
x : α
⊢ f x * c * c⁻¹ = f x
[PROOFSTEP]
simp [mul_assoc, mul_inv_cancel hc0]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Field β
inst✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n => c * f n
x : α
⊢ c⁻¹ * (c * f x) = f x
[PROOFSTEP]
simp [← mul_assoc, inv_mul_cancel hc0]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
[PROOFSTEP]
refine'
  ⟨fun h z => Tendsto.isBoundedUnder_le (Tendsto.abs (h z)), fun h =>
    (superpolynomialDecay_iff_abs_tendsto_zero l k f).2 fun z => _⟩
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
[PROOFSTEP]
obtain ⟨m, hm⟩ := h (z + 1)
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
[PROOFSTEP]
have h1 : Tendsto (fun _ : α => (0 : β)) l (𝓝 0) := tendsto_const_nhds
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
[PROOFSTEP]
have h2 : Tendsto (fun a : α => |(k a)⁻¹| * m) l (𝓝 0) :=
  zero_mul m ▸ Tendsto.mul_const m ((tendsto_zero_iff_abs_tendsto_zero _).1 hk.inv_tendsto_atTop)
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
[PROOFSTEP]
refine'
  tendsto_of_tendsto_of_tendsto_of_le_of_le' h1 h2 (eventually_of_forall fun x => abs_nonneg _)
    ((eventually_map.1 hm).mp _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
⊢ ∀ᶠ (x : α) in l, (fun x x_1 => x ≤ x_1) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m
[PROOFSTEP]
refine' (hk.eventually_ne_atTop 0).mono fun x hk0 hx => _
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x x_1 => x ≤ x_1) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| ≤ |(k x)⁻¹| * m
[PROOFSTEP]
refine' Eq.trans_le _ (mul_le_mul_of_nonneg_left hx <| abs_nonneg (k x)⁻¹)
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x x_1 => x ≤ x_1) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
[PROOFSTEP]
rw [← abs_mul, ← mul_assoc, pow_succ, ← mul_assoc, inv_mul_cancel hk0, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
refine' ⟨fun h z => _, fun h n => by simpa only [zpow_ofNat] using h (n : ℤ)⟩
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
n : ℕ
⊢ Tendsto (fun a => k a ^ n * f a) l (𝓝 0)
[PROOFSTEP]
simpa only [zpow_ofNat] using h (n : ℤ)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
by_cases hz : 0 ≤ z
[GOAL]
case pos
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : 0 ≤ z
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
unfold Tendsto
[GOAL]
case pos
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : 0 ≤ z
⊢ Filter.map (fun a => k a ^ z * f a) l ≤ 𝓝 0
[PROOFSTEP]
lift z to ℕ using hz
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℕ
⊢ Filter.map (fun a => k a ^ ↑z * f a) l ≤ 𝓝 0
[PROOFSTEP]
simpa using h z
[GOAL]
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : ¬0 ≤ z
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
have : Tendsto (fun a => k a ^ z) l (𝓝 0) := Tendsto.comp (tendsto_zpow_atTop_zero (not_le.1 hz)) hk
[GOAL]
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : ¬0 ≤ z
this : Tendsto (fun a => k a ^ z) l (𝓝 0)
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
have h : Tendsto f l (𝓝 0) := by simpa using h 0
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : ¬0 ≤ z
this : Tendsto (fun a => k a ^ z) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
[PROOFSTEP]
simpa using h 0
[GOAL]
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h✝ : SuperpolynomialDecay l k f
z : ℤ
hz : ¬0 ≤ z
this : Tendsto (fun a => k a ^ z) l (𝓝 0)
h : Tendsto f l (𝓝 0)
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
exact zero_mul (0 : β) ▸ this.mul h
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
z : ℤ
⊢ SuperpolynomialDecay l k fun a => k a ^ z * f a
[PROOFSTEP]
rw [superpolynomialDecay_iff_zpow_tendsto_zero _ hk] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto (fun a => k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)
[PROOFSTEP]
refine' fun z' => (hf <| z' + z).congr' ((hk.eventually_ne_atTop 0).mono fun x hx => _)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z z' : ℤ
x : α
hx : k x ≠ 0
⊢ k x ^ (z' + z) * f x = (fun a => k a ^ z' * (k a ^ z * f a)) x
[PROOFSTEP]
simp [zpow_add₀ hx, mul_assoc, Pi.mul_apply]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k⁻¹ * f)
[PROOFSTEP]
simpa using hf.param_zpow_mul hk (-1)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k (k * f)
x : α
hx : k x ≠ 0
⊢ (k⁻¹ * (k * f)) x = f x
[PROOFSTEP]
simp [← mul_assoc, inv_mul_cancel hx]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
simpa [mul_comm k] using superpolynomialDecay_param_mul_iff f hk
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (k ^ Nat.zero * f) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ Nat.succ n * f) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
simpa [pow_succ, ← mul_comm k, mul_assoc, superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
simpa [mul_comm f] using superpolynomialDecay_param_pow_mul_iff f hk n
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝ : NormedLinearOrderedField β
⊢ (∀ (n : ℕ), Tendsto (fun a => ‖k a ^ n * f a‖) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a => ‖k a‖) fun a => ‖f a‖
[PROOFSTEP]
simp [SuperpolynomialDecay]
[GOAL]
α : 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
[PROOFSTEP]
refine' (superpolynomialDecay_iff_zpow_tendsto_zero f hk).trans _
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ (∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z
[PROOFSTEP]
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ (∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z
[PROOFSTEP]
refine' ⟨fun h z => _, fun h z => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ f =O[l] fun a => k a ^ z
[PROOFSTEP]
refine' isBigO_of_div_tendsto_nhds (hk0.mono fun x hx hxz => absurd (zpow_eq_zero hxz) hx) 0 _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ Tendsto (f / fun a => k a ^ z) l (𝓝 0)
[PROOFSTEP]
have : (fun a : α => k a ^ z)⁻¹ = fun a : α => k a ^ (-z) := funext fun x => by simp
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
x : α
⊢ (fun a => k a ^ z)⁻¹ x = k x ^ (-z)
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a => k a ^ z)⁻¹ = fun a => k a ^ (-z)
⊢ Tendsto (f / fun a => k a ^ z) l (𝓝 0)
[PROOFSTEP]
rw [div_eq_mul_inv, mul_comm f, this]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a => k a ^ z)⁻¹ = fun a => k a ^ (-z)
⊢ Tendsto ((fun a => k a ^ (-z)) * f) l (𝓝 0)
[PROOFSTEP]
exact h (-z)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
suffices : (fun a : α => k a ^ z * f a) =O[l] fun a : α => (k a)⁻¹
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
this : (fun a => k a ^ z * f a) =O[l] fun a => (k a)⁻¹
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
case this
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ (fun a => k a ^ z * f a) =O[l] fun a => (k a)⁻¹
[PROOFSTEP]
exact IsBigO.trans_tendsto this hk.inv_tendsto_atTop
[GOAL]
case this
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ (fun a => k a ^ z * f a) =O[l] fun a => (k a)⁻¹
[PROOFSTEP]
refine' ((isBigO_refl (fun a => k a ^ z) l).mul (h (-(z + 1)))).trans (IsBigO.of_bound 1 <| hk0.mono fun a ha0 => _)
[GOAL]
case this
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
a : α
ha0 : k a ≠ 0
⊢ ‖k a ^ z * k a ^ (-(z + 1))‖ ≤ 1 * ‖(k a)⁻¹‖
[PROOFSTEP]
simp only [one_mul, neg_add z 1, zpow_add₀ ha0, ← mul_assoc, zpow_neg, mul_inv_cancel (zpow_ne_zero z ha0), zpow_one]
[GOAL]
case this
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
a : α
ha0 : k a ≠ 0
⊢ ‖(k a)⁻¹‖ ≤ ‖(k a)⁻¹‖
[PROOFSTEP]
rfl
[GOAL]
α : 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
[PROOFSTEP]
refine' ⟨fun h z => _, fun h => (superpolynomialDecay_iff_isBigO f hk).2 fun z => (h z).isBigO⟩
[GOAL]
α : 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
[PROOFSTEP]
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
[GOAL]
α : 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
[PROOFSTEP]
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)
[GOAL]
α : 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)
[PROOFSTEP]
simpa using hk.inv_tendsto_atTop
[GOAL]
α : 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
[PROOFSTEP]
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)
[GOAL]
α : 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)
[PROOFSTEP]
simpa using this.mul_isBigO ((superpolynomialDecay_iff_isBigO f hk).1 h <| z - 1)
[GOAL]
α : 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
[PROOFSTEP]
refine' this.trans_isBigO (IsBigO.of_bound 1 (hk0.mono fun x hkx => le_of_eq _))
[GOAL]
α : 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‖
[PROOFSTEP]
rw [one_mul, zpow_sub_one₀ hkx, mul_comm (k x), mul_assoc, inv_mul_cancel hkx, mul_one]
