-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_iff_abs_isBoundedUnder (hk : Tendsto k l atTop) :
    SuperpolynomialDecay l k f ↔
    ∀ z : ℕ, IsBoundedUnder (· ≤ ·) l fun a : α => |k a ^ z * f a|

Proof state:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) 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)

Tactic:
refine
  tendsto_of_tendsto_of_tendsto_of_le_of_le' h1 h2 (Eventually.of_forall fun x => abs_nonneg _)
    ((eventually_map.1 hm).mp ?_)

Result:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
⊢ ∀ᶠ (x : α) in l, (fun x1 x2 => x1 ≤ x2) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m

Proof state:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| ≤ |(k x)⁻¹| * m

Tactic:
refine Eq.trans_le ?_ (mul_le_mul_of_nonneg_left hx <| abs_nonneg (k x)⁻¹)

Result:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun a => |k a ^ z * f a|

Tactic:
refine
  ⟨fun h z => Tendsto.isBoundedUnder_le (Tendsto.abs (h z)), fun h =>
    (superpolynomialDecay_iff_abs_tendsto_zero l k f).2 fun z => ?_⟩

Result:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun a => |k a ^ z * f a|
z : ℕ
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)

Proof state:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|

Tactic:
rw [← abs_mul, ← mul_assoc, pow_succ', ← mul_assoc, inv_mul_cancel₀ hk0, one_mul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun a => |k a ^ z * f a|
z : ℕ
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)

Tactic:
obtain ⟨m, hm⟩ := h (z + 1)

Result:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) x m
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)

Proof state:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)

Tactic:
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)

Result:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) 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)

Proof state:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) x m
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)

Tactic:
have h1 : Tendsto (fun _ : α => (0 : β)) l (𝓝 0) := tendsto_const_nhds

Result:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)

Proof state:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
⊢ ∀ᶠ (x : α) in l, (fun x1 x2 => x1 ≤ x2) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m

Tactic:
refine (hk.eventually_ne_atTop 0).mono fun x hk0 hx => ?_

Result:
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) 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 x1 x2 => x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| ≤ |(k x)⁻¹| * m