-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_iff_zpow_tendsto_zero (hk : Tendsto k l atTop) :
    SuperpolynomialDecay l k f ↔ ∀ z : ℤ, Tendsto (fun a : α => k a ^ z * f a) l (𝓝 0)

Proof state:
case pos.intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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

Tactic:
simpa using h z

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 : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
n : ℕ
⊢ Tendsto (fun a => k a ^ n * f a) l (𝓝 0)

Tactic:
simpa only [zpow_natCast] using h (n : ℤ)

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

Tactic:
exact zero_mul (0 : β) ▸ this.mul h

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

Tactic:
have : Tendsto (fun a => k a ^ z) l (𝓝 0) :=
  Tendsto.comp (tendsto_zpow_atTop_zero (not_le.1 hz)) hk

Result:
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

Proof state:
case pos
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

Tactic:
unfold Tendsto

Result:
case pos
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

Tactic:
simpa using h 0

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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

Tactic:
lift z to ℕ using hz

Result:
case pos.intro
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

Tactic:
by_cases hz : 0 ≤ z

Result:
case pos
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

case neg
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

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 : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)

Tactic:
refine ⟨fun h z => ?_, fun h n => by simpa only [zpow_natCast] using h (n : ℤ)⟩

Result:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

Proof state:
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)

Tactic:
have h : Tendsto f l (𝓝 0) := by simpa using h 0

Result:
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
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)