awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : 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.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (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
rw : |k x ^ z * f x| = |(k x)⁻¹ * (k x ^ (z + 1) * f x)|
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
have rw₁ : |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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : 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.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (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
rw : |k x ^ z * f x| = |(k x)⁻¹ * (k x ^ (z + 1) * f x)|
rw₁ : |k x ^ z * f x| = |(k x)⁻¹ * k x ^ (z + 1) * f x|
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
have rw₂ : |k x ^ z * f x| = |(k x)⁻¹ * (k x * k x ^ z) * f x|
Tactic: rw [← abs_mul, ← mul_assoc, pow_succ', ← mul_assoc, inv_mul_cancel₀ hk0, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : 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.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (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
rw : |k x ^ z * f x| = |(k x)⁻¹ * (k x ^ (z + 1) * f x)|
rw₁ : |k x ^ z * f x| = |(k x)⁻¹ * k x ^ (z + 1) * f x|
rw₂ : |k x ^ z * f x| = |(k x)⁻¹ * (k x * k x ^ z) * f x|
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
have rw₃ : |k x ^ z * f x| = |(k x)⁻¹ * k x * k x ^ z * f x|
Tactic: rw [← abs_mul, ← mul_assoc, pow_succ', ← mul_assoc, inv_mul_cancel₀ hk0, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : 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.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (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
rw : |k x ^ z * f x| = |(k x)⁻¹ * (k x ^ (z + 1) * f x)|
rw₁ : |k x ^ z * f x| = |(k x)⁻¹ * k x ^ (z + 1) * f x|
rw₂ : |k x ^ z * f x| = |(k x)⁻¹ * (k x * k x ^ z) * f x|
rw₃ : |k x ^ z * f x| = |(k x)⁻¹ * k x * k x ^ z * f x|
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
have rw₄ : |k x ^ z * f x| = |1 * k x ^ z * f x|
Tactic: rw [← abs_mul, ← mul_assoc, pow_succ', ← mul_assoc, inv_mul_cancel₀ hk0, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : 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.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (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
rw : |k x ^ z * f x| = |(k x)⁻¹ * (k x ^ (z + 1) * f x)|
rw₁ : |k x ^ z * f x| = |(k x)⁻¹ * k x ^ (z + 1) * f x|
rw₂ : |k x ^ z * f x| = |(k x)⁻¹ * (k x * k x ^ z) * f x|
rw₃ : |k x ^ z * f x| = |(k x)⁻¹ * k x * k x ^ z * f x|
rw₄ : |k x ^ z * f x| = |1 * k x ^ z * f x|
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
have rw₅ : |k x ^ z * f x| = |k x ^ z * f x|
Tactic: rw [← abs_mul, ← mul_assoc, pow_succ', ← mul_assoc, inv_mul_cancel₀ hk0, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
have refine : ∀ (h : SuperpolynomialDecay l k f) (z : ℤ), Tendsto.{u_1, u_2} (β := β) (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 : ℤ)⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
have pos : ∀ (hz : 0 ≤ z), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
Tactic: by_cases! hz : 0 ≤ z
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
pos : ∀ (hz : 0 ≤ z), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
have neg : ∀ (hz : z < 0), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
Tactic: by_cases! hz : 0 ≤ z
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : 0 ≤ z
⊢ LE.le.{u_2} (α := Filter β) (Filter.map (fun (a : α) ↦ k a ^ z * f a) l) (𝓝 0)
have pos : ∀ (z : ℕ), LE.le.{u_2} (α := Filter β) (Filter.map (fun (a : α) ↦ HPow.hPow (β := ℤ) (k a) (↑z : ℤ) * f a) l) (𝓝 0)
Tactic: lift z to ℕ using hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (hypothesis)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
have this : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z) l (𝓝 0)
Tactic: have : Tendsto (fun a => k a ^ z) l (𝓝 0) :=
      Tendsto.comp (tendsto_zpow_atTop_zero hz) hk
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (hypothesis)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
this : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
have h₁ : Tendsto f l (𝓝 0)
Tactic: have h : Tendsto f l (𝓝 0) := by simpa using h 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
z : ℤ
⊢ SuperpolynomialDecay l k fun (a : α) ↦ k a ^ z * f a
have rw : ∀ (hf : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) (z z_1 : ℤ),
  Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)
Tactic: rw [superpolynomialDecay_iff_zpow_tendsto_zero _ hk] at hf ⊢
Cleared hypotheses: hf, z
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)
have refine : ∀ (z' : ℤ) (x : α) (hx : k x ≠ 0), k x ^ (z' + z) * f x = (fun (a : α) ↦ k a ^ z' * (k a ^ z * f a)) x
Tactic: refine fun z' => (hf <| z' + z).congr' ((hk.eventually_ne_atTop 0).mono fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
have zero : SuperpolynomialDecay l k (HPow.hPow (β := ℕ) k 0 * f) ↔ SuperpolynomialDecay l k f
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    simpa [pow_succ, ← mul_comm k, mul_assoc,
      superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
zero : SuperpolynomialDecay l k (HPow.hPow (β := ℕ) k 0 * f) ↔ SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
have succ : ∀ (n : ℕ) (hn : SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f),
  SuperpolynomialDecay l k (k ^ (n + 1) * f) ↔ SuperpolynomialDecay l k f
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    simpa [pow_succ, ← mul_comm k, mul_assoc,
      superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
have refine : (∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) ↔
  ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
Tactic: refine (superpolynomialDecay_iff_zpow_tendsto_zero f hk).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (hypothesis)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
⊢ (∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) ↔
    ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
have hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
Tactic: have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ (∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) ↔
    ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
have refine_1 : ∀ (h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) (z : ℤ),
  IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
Tactic: refine ⟨fun h z => ?_, fun h z => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
refine_1 :
  ∀ (h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) (z : ℤ),
    IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
⊢ (∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) ↔
    ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
have refine_2 : ∀ (h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z) (z : ℤ),
  Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
Tactic: refine ⟨fun h z => ?_, fun h z => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
have refine_1 : Tendsto (f / fun (a : α) ↦ k a ^ z) l (𝓝 0)
Tactic: refine isBigO_of_div_tendsto_nhds (hk0.mono fun x hx hxz ↦ absurd hxz (zpow_ne_zero _ hx)) 0 ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (hypothesis)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ Tendsto (f / fun (a : α) ↦ k a ^ z) l (𝓝 0)
have this : Eq (α := (a : α) → β) (fun (a : α) ↦ k a ^ z)⁻¹ fun (a : α) ↦ k a ^ (-z)
Tactic: have : (fun a : α => k a ^ z)⁻¹ = fun a : α => k a ^ (-z) := funext fun x => by simp
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : Eq (α := (a : α) → β) (fun (a : α) ↦ k a ^ z)⁻¹ fun (a : α) ↦ k a ^ (-z)
⊢ Tendsto (f / fun (a : α) ↦ k a ^ z) l (𝓝 0)
have refine_1 : Tendsto ((fun (a : α) ↦ k a ^ (-z)) * f) l (𝓝 0)
Tactic: rw [div_eq_mul_inv, mul_comm f, this]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
z : ℤ
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
have refine_2 : IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (a : α) ↦ k a ^ z * f a) fun (a : α) ↦ (k a)⁻¹
Tactic: suffices (fun a : α => k a ^ z * f a) =O[l] fun a : α => (k a)⁻¹ from
      IsBigO.trans_tendsto this hk.inv_tendsto_atTop
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
z : ℤ
⊢ IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (a : α) ↦ k a ^ z * f a) fun (a : α) ↦ (k a)⁻¹
have refine_2 : IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (x : α) ↦ k x ^ z * k x ^ (-(z + 1))) fun (a : α) ↦ (k a)⁻¹
Tactic: refine ((isBigO_refl (fun a => k a ^ z) l).mul (h (-(z + 1)))).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
z : ℤ
⊢ IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (x : α) ↦ k x ^ z * k x ^ (-(z + 1))) fun (a : α) ↦ (k a)⁻¹
have refine_2 : ∀ (a : α) (ha0 : k a ≠ 0), ‖k a ^ z * k a ^ (-(z + 1))‖ ≤ ‖(k a)⁻¹‖
Tactic: refine .of_bound' <| hk0.mono fun a ha0 => ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z
have refine : ∀ (h : SuperpolynomialDecay l k f) (z : ℤ), IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z
Tactic: refine ⟨fun h z => ?_, fun h => (superpolynomialDecay_iff_isBigO f hk).2 fun z => (h z).isBigO⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (hypothesis)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
⊢ IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z
have hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
Tactic: have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (hypothesis)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z
have this : IsLittleO (E := β) l (fun (x : α) ↦ 1) k
Tactic: 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)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (hypothesis)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : IsLittleO (E := β) l (fun (x : α) ↦ 1) k
⊢ IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z
have this₁ : IsLittleO (F := β) l f fun (x : α) ↦ k x * k x ^ (z - 1)
Tactic: 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)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this_1 : IsLittleO (E := β) l (fun (x : α) ↦ 1) k
this : IsLittleO (F := β) l f fun (x : α) ↦ k x * k x ^ (z - 1)
⊢ IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z
have refine : ∀ (x : α) (hkx : k x ≠ 0), ‖k x * k x ^ (z - 1)‖ = ‖k x ^ z‖
Tactic: refine this.trans_isBigO <| IsBigO.of_bound' <| hk0.mono fun x hkx => le_of_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
⊢ f =o[𝕜; l] g ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x) / egauge 𝕜 V (g x)) l (𝓝 0)
have simp : (∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ ⊥ →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
                (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) ↔
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (i : ℝ≥0), ⊥ < i → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) / egauge 𝕜 V (g x) ∈ ENNReal.ofNNReal '' Iic i
Tactic: simp only [isLittleOTVS_iff, ← ENNReal.coe_zero, ENNReal.nhds_coe, ← NNReal.bot_eq_zero,
    (nhds_bot_basis_Iic.map _).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)
have obtain : ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
  (hV :
    ∀ (ε : ℝ≥0),
      ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)),
  ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)
Tactic: obtain ⟨V, hV₀, hV⟩ := h.exists_eventuallyLE_mul U hU
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)
have refine : ∀ (ε : ℝ≥0∞) (hε : ε ≠ 0),
  l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)
Tactic: refine ⟨V, hV₀, fun ε hε ↦ ?_⟩