awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
h₁ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (HSMul.hSMul (α := ℝ) (↑n : ℝ) l) = l
h₂ : HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) • l = l
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (n • l) = l
have h₃ : HSMul.hSMul (α := ℝ) 1 l = l
Tactic: rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul, inv_mul_cancel₀ nposℝ.ne', one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
h₁ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (HSMul.hSMul (α := ℝ) (↑n : ℝ) l) = l
h₂ : HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) • l = l
h₃ : HSMul.hSMul (α := ℝ) 1 l = l
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (n • l) = l
have h₄ : l = l
Tactic: rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul, inv_mul_cancel₀ nposℝ.ne', one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑x : ℝ)⁻¹ (↑x : ℝ)) fun (_x : ℕ) ↦ 1
have h₁ : ∀ (n : ℕ) (npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n), HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = 1
Tactic: filter_upwards [Ici_mem_atTop 1] with n npos
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = 1
have nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = 1
have h₁ : HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = 1
Tactic: rw [smul_eq_mul, inv_mul_cancel₀ nposℝ.ne']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
h₁ : HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = 1
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = 1
have h₂ : Eq (α := ℝ) 1 1
Tactic: rw [smul_eq_mul, inv_mul_cancel₀ nposℝ.ne']
-- 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 : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f)
have zero : SuperpolynomialDecay l k (HPow.hPow (β := ℕ) k 0 * f)
Tactic: induction n with
  | zero => simpa only [one_mul, pow_zero] using hf
  | succ n hn => simpa only [pow_succ', mul_assoc] using hn.param_mul
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 : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
zero : SuperpolynomialDecay l k (HPow.hPow (β := ℕ) k 0 * f)
⊢ SuperpolynomialDecay l k (k ^ n * f)
have succ : ∀ (n : ℕ) (hn : SuperpolynomialDecay l k (k ^ n * f)), SuperpolynomialDecay l k (k ^ (n + 1) * f)
Tactic: induction n with
  | zero => simpa only [one_mul, pow_zero] using hf
  | succ n hn => simpa only [pow_succ', mul_assoc] using hn.param_mul
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : g x ≤ f x
⊢ 0 x ≤ k x → k x ^ z * g x ≤ k x ^ z * f x
have h : ∀ (hx' : 0 ≤ k x), k x ^ z * g x ≤ k x ^ z * f x
Tactic: (hx' : 0 ≤ k x)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : g x ≤ f x
hx' : 0 ≤ k x
⊢ k x ^ z * g x ≤ k x ^ z * f x
have ha : 0 ≤ k x ^ z
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
⊢ ∀ᶠ (b : α) in l, k b ^ z * g b ≤ k b ^ z * f b
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≤ f x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ k x) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ k b ^ z * g b ≤ k b ^ z * f b) x} x}
          x}
    a
Tactic: filter_upwards [hfg, hk] with x hx (hx' : 0 ≤ k x) using by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≤ f x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ k x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ k b ^ z * g b ≤ k b ^ z * f b) x} x}
            x}
      a
⊢ ∀ᶠ (b : α) in l, k b ^ z * g b ≤ k b ^ z * f b
have h₁ : ∀ (a : α), g a ≤ f a → 0 a ≤ k a → k a ^ z * g a ≤ k a ^ z * f a
Tactic: filter_upwards [hfg, hk] with x hx (hx' : 0 ≤ k x) using by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≤ f x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ k x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ k b ^ z * g b ≤ k b ^ z * f b) x} x}
            x}
      a
h₁ : ∀ (a : α), g a ≤ f a → 0 a ≤ k a → k a ^ z * g a ≤ k a ^ z * f a
⊢ ∀ᶠ (b : α) in l, k b ^ z * g b ≤ k b ^ z * f b
have h₂ : ∀ (x : α) (hx : g x ≤ f x) (hx' : 0 ≤ k x), k x ^ z * g x ≤ k x ^ z * f x
Tactic: filter_upwards [hfg, hk] with x hx (hx' : 0 ≤ k x) using by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : f x ≤ g' x
⊢ 0 x ≤ k x → k x ^ z * f x ≤ k x ^ z * g' x
have h : ∀ (hx' : 0 ≤ k x), k x ^ z * f x ≤ k x ^ z * g' x
Tactic: (hx' : 0 ≤ k x)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : f x ≤ g' x
hx' : 0 ≤ k x
⊢ k x ^ z * f x ≤ k x ^ z * g' x
have ha : 0 ≤ k x ^ z
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
⊢ ∀ᶠ (b : α) in l, k b ^ z * f b ≤ k b ^ z * g' b
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g' x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ k x) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ k b ^ z * f b ≤ k b ^ z * g' b) x} x}
          x}
    a
Tactic: filter_upwards [hfg', hk] with x hx (hx' : 0 ≤ k x) using by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g' x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ k x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ k b ^ z * f b ≤ k b ^ z * g' b) x} x}
            x}
      a
⊢ ∀ᶠ (b : α) in l, k b ^ z * f b ≤ k b ^ z * g' b
have h₁ : ∀ (a : α), f a ≤ g' a → 0 a ≤ k a → k a ^ z * f a ≤ k a ^ z * g' a
Tactic: filter_upwards [hfg', hk] with x hx (hx' : 0 ≤ k x) using by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g' x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ k x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ k b ^ z * f b ≤ k b ^ z * g' b) x} x}
            x}
      a
h₁ : ∀ (a : α), f a ≤ g' a → 0 a ≤ k a → k a ^ z * f a ≤ k a ^ z * g' a
⊢ ∀ᶠ (b : α) in l, k b ^ z * f b ≤ k b ^ z * g' b
have h₂ : ∀ (x : α) (hx : f x ≤ g' x) (hx' : 0 ≤ k x), k x ^ z * f x ≤ k x ^ z * g' x
Tactic: filter_upwards [hfg', hk] with x hx (hx' : 0 ≤ k x) using by gcongr
-- 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 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
⊢ (∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)) ↔
    SuperpolynomialDecay.{u_1, u_2} (β := β) l (fun (a : α) ↦ |k a|) fun (a : α) ↦ |f a|
have simp_rw : (∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)) ↔
  ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a| ^ n * |f a|) l (𝓝 0)
Tactic: simp_rw [SuperpolynomialDecay, abs_mul, abs_pow]
-- 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 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
simp_rw :
  (∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)) ↔
    ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a| ^ n * |f a|) l (𝓝 0)
⊢ (∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)) ↔
    SuperpolynomialDecay.{u_1, u_2} (β := β) l (fun (a : α) ↦ |k a|) fun (a : α) ↦ |f a|
have simp_rw₁ : (∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n| * |f a|) l (𝓝 0)) ↔
  ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a| ^ n * |f a|) l (𝓝 0)
Tactic: simp_rw [SuperpolynomialDecay, abs_mul, abs_pow]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : SuperpolynomialDecay l k f
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ SuperpolynomialDecay l k g
have rw : ∀ (hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)) (hfg : abs ∘ g ≤ᶠ[l] abs ∘ f)
  (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * g a|) l (𝓝 0)
Tactic: rw [superpolynomialDecay_iff_abs_tendsto_zero] at hf ⊢
Cleared hypotheses: hf, hfg
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * g a|) l (𝓝 0)
have refine : ∀ (z : ℕ) (x : α) (hx : (abs ∘ g) x ≤ (abs ∘ f) x), |k x ^ z * g x| ≤ |k x ^ z * f x|
Tactic: 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 => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (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|
have hbc : |g x| ≤ |f x|
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SuperpolynomialDecay (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (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|
have x₁ : |k x ^ z| * |g x| ≤ |k x ^ z| * |f x|
Tactic: 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
-- 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 : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
have h : ∀ (h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|) (z : ℕ),
  Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)
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 => ?_⟩
-- 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 : ℕ
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)
have obtain : ∀ (m : β) (hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m),
  Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)
Tactic: obtain ⟨m, hm⟩ := h (z + 1)
-- 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 : ∀ (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.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)
have h1 : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
Tactic: have h1 : Tendsto (fun _ : α => (0 : β)) l (𝓝 0) := tendsto_const_nhds
-- 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 : ∀ (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)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)
have h2 : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |(k a)⁻¹| * m) 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)
-- 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)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)
have tendsto_of_tendsto_of_tendsto_of_le_of_le' : ∀ᶠ (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
    tendsto_of_tendsto_of_tendsto_of_le_of_le' h1 h2 (Eventually.of_forall fun x => abs_nonneg _)
      ((eventually_map.1 hm).mp ?_)
-- 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 : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m
have refine : ∀ (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 (hk.eventually_ne_atTop 0).mono fun x hk0 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
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
⊢ |k x ^ z * f x| ≤ |(k x)⁻¹| * m
have refine : |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
Tactic: refine Eq.trans_le ?_ (mul_le_mul_of_nonneg_left hx <| abs_nonneg (k x)⁻¹)
-- 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
⊢ |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]