awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0∞
ha : a ∈ Set.Ioi (↑c : ℝ≥0∞)
ha' : ¬a = ∞
⊢ (↑x : ℝ≥0∞) < a ^ y
have neg : ∀ (a : ℝ≥0) (ha : (↑a : ℝ≥0∞) ∈ Set.Ioi (↑c : ℝ≥0∞)), (↑x : ℝ≥0∞) < (↑a : ℝ≥0∞) ^ y
Tactic: lift a to ℝ≥0 using ha'
Cleared hypotheses: a, ha, ha'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0
ha : (↑a : ℝ≥0∞) ∈ Set.Ioi (↑c : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞) < (↑a : ℝ≥0∞) ^ y
have ha₁ : c < a
Tactic: simp only [Set.mem_Ioi, coe_lt_coe] at ha hc
Cleared hypotheses: hc, ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0
ha : (↑a : ℝ≥0∞) ∈ Set.Ioi (↑c : ℝ≥0∞)
ha₁ : c < a
⊢ (↑x : ℝ≥0∞) < (↑a : ℝ≥0∞) ^ y
have hc₁ : ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y
Tactic: simp only [Set.mem_Ioi, coe_lt_coe] at ha hc
Cleared hypotheses: hc, ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y
⊢ (↑x : ℝ≥0∞) < (↑a : ℝ≥0∞) ^ y
have neg : (↑x : ℝ≥0∞) < (↑(a ^ y) : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_rpow_of_nonneg _ hy.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ |(g x).im|
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ rexp ((f x).arg * (g x).im)) fun (x : α) ↦ 1
have rcases : ∀ (b : ℝ) (hb : ∀ᶠ (x : ℝ) in Filter.map (fun (x : α) ↦ |(g x).im|) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x b),
  IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ rexp ((f x).arg * (g x).im)) fun (x : α) ↦ 1
Tactic: rcases hl with ⟨b, hb⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun (x : α) ↦ |(g x).im|) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x b
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ rexp ((f x).arg * (g x).im)) fun (x : α) ↦ 1
have refine : ∀ᶠ (x : ℝ) in Filter.map (fun (x : α) ↦ |(f x).arg * (g x).im|) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (π * b)
Tactic: refine Real.isTheta_exp_comp_one.2 ⟨π * b, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun (x : α) ↦ |(g x).im|) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x b
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun (x : α) ↦ |(f x).arg * (g x).im|) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (π * b)
have rw : ∀ (hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(g a).im| b),
  ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(f a).arg * (g a).im| (π * b)
Tactic: rw [eventually_map] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(g a).im| b
⊢ ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(f a).arg * (g a).im| (π * b)
have refine : ∀ (x : α) (hx : (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(g x).im| b), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(f x).arg * (g x).im| (π * b)
Tactic: refine hb.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(g a).im| b
x : α
hx : (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(g x).im| b
⊢ (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(f x).arg * (g x).im| (π * b)
have rw : (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (|(f x).arg| * |(g x).im|) (π * b)
Tactic: rw [abs_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ IsBigOWith (E := ℝ) (F := ℝ) (c ^ r) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
have a : ∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
Tactic: apply IsBigOWith.of_bound
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ ∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
have h₁ : ∀ (x : α) (hgx : 0 x ≤ g x) (hx : ‖f x‖ ≤ c * ‖g x‖), ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
Tactic: filter_upwards [hg, h.bound] with x hgx hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ |f x| ^ r ≤ (c * |g x|) ^ r
have h₁ : |f x| ≤ c * |g x|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (c * |g x|) ^ r = c ^ r * |g x ^ r|
have rw : c ^ r * |g x| ^ r = c ^ r * |g x ^ r|
Tactic: rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
rw : c ^ r * |g x| ^ r = c ^ r * |g x ^ r|
⊢ (c * |g x|) ^ r = c ^ r * |g x ^ r|
have rw₁ : c ^ r * |g x| ^ r = c ^ r * |g x| ^ r
Tactic: rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
have x₁ : |f x| ^ r ≤ (c * |g x|) ^ r
Tactic: calc
    |f x ^ r| ≤ |f x| ^ r := abs_rpow_le_abs_rpow _ _
    _ ≤ (c * |g x|) ^ r := by gcongr; assumption
    _ = c ^ r * |g x ^ r| := by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
x₁ : |f x| ^ r ≤ (c * |g x|) ^ r
⊢ ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
have x₂ : (c * |g x|) ^ r = c ^ r * |g x ^ r|
Tactic: calc
    |f x ^ r| ≤ |f x| ^ r := abs_rpow_le_abs_rpow _ _
    _ ≤ (c * |g x|) ^ r := by gcongr; assumption
    _ = c ^ r * |g x ^ r| := by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
have inr : ∀
  (rpow_pos :
    ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g)
      (hr : r ≥ 0), IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r)
  (hr : ¬r ≥ 0), IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
Tactic: wlog hr : r ≥ 0 with rpow_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
inr :
  ∀
    (rpow_pos :
      ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g)
        (hr : r ≥ 0), IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r)
    (hr : ¬r ≥ 0), IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
have wlog : ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g) (hr : r ≥ 0),
  IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
Tactic: wlog hr : r ≥ 0 with rpow_pos
Cleared hypotheses: hf, hg, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g) (hr : r ≥ 0),
    IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
hr : ¬r ≥ 0
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
have inr : IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (f x ^ r)⁻¹) fun (x : α) ↦ (g x ^ r)⁻¹
Tactic: rw [← isTheta_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g) (hr : r ≥ 0),
    IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
hr : ¬r ≥ 0
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (f x ^ r)⁻¹) fun (x : α) ↦ (g x ^ r)⁻¹
have inr : IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ (-r)) fun (x : α) ↦ (g x ^ r)⁻¹
Tactic: grw [← EventuallyEq.isTheta <| hf.mono fun x hfx ↦ Real.rpow_neg hfx r]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g) (hr : r ≥ 0),
    IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
hr : ¬r ≥ 0
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ (-r)) fun (x : α) ↦ (g x ^ r)⁻¹
have inr : IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ (-r)) fun (x : α) ↦ g x ^ (-r)
Tactic: grw [← EventuallyEq.isTheta <| hg.mono fun x hgx ↦ Real.rpow_neg hgx r]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g) (hr : r ≥ 0),
    IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
hr : ¬r ≥ 0
⊢ -r ≥ 0
have linarith : -r < 0 → r - 0 + (-r - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
have refine : ∀ (c : ℝ) (hc : 0 < c), IsBigOWith (E := ℝ) (F := ℝ) c l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
Tactic: refine .of_isBigOWith fun c hc ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith (E := ℝ) (F := ℝ) c l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
have rw : IsBigOWith (E := ℝ) (F := ℝ) ((c ^ r⁻¹) ^ r) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
Tactic: rw [← rpow_inv_rpow hc.le hr.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith (E := ℝ) (F := ℝ) ((c ^ r⁻¹) ^ r) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
have refine_1 : 0 < c ^ r⁻¹
Tactic: refine (h.forall_isBigOWith ?_).rpow ?_ ?_ hg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
refine_1 : 0 < c ^ r⁻¹
⊢ IsBigOWith (E := ℝ) (F := ℝ) ((c ^ r⁻¹) ^ r) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
have refine_2 : 0 ≤ c ^ r⁻¹
Tactic: refine (h.forall_isBigOWith ?_).rpow ?_ ?_ hg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
refine_1 : 0 < c ^ r⁻¹
refine_2 : 0 ≤ c ^ r⁻¹
⊢ IsBigOWith (E := ℝ) (F := ℝ) ((c ^ r⁻¹) ^ r) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
have refine_3 : 0 ≤ r
Tactic: refine (h.forall_isBigOWith ?_).rpow ?_ ?_ hg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun (n : ℕ) ↦ g n / (↑(HPow.hPow (α := ℝ) (↑n : ℝ) r) : 𝕜)) atTop (𝓝 a)
⊢ IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
have refine_1 : ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := ℝ) (↑x : ℝ) r = 0 → ‖g x‖ = 0
Tactic: refine (isBigO_of_div_tendsto_nhds ?_ ‖a‖ ?_).of_norm_left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun (n : ℕ) ↦ g n / (↑(HPow.hPow (α := ℝ) (↑n : ℝ) r) : 𝕜)) atTop (𝓝 a)
refine_1 : ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := ℝ) (↑x : ℝ) r = 0 → ‖g x‖ = 0
⊢ IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
have refine_2 : Tendsto (HDiv.hDiv (α := ℕ → ℝ) (fun (x : ℕ) ↦ ‖g x‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r) atTop (𝓝 ‖a‖)
Tactic: refine (isBigO_of_div_tendsto_nhds ?_ ‖a‖ ?_).of_norm_left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun (n : ℕ) ↦ g n / (↑(HPow.hPow (α := ℝ) (↑n : ℝ) r) : 𝕜)) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := ℝ) (↑x : ℝ) r = 0 → ‖g x‖ = 0
have h : ∀ (a : ℕ) (h : a ≠ 0), HPow.hPow (α := ℝ) (↑a : ℝ) r = 0 → ‖g a‖ = 0
Tactic: filter_upwards [eventually_ne_atTop 0] with _ h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : IsBigO (F := ℝ) atTop f fun (t : ℝ) ↦ t ^ a
hg : IsBigO (F := ℝ) atTop g fun (t : ℝ) ↦ t ^ b
h : a + b ≤ c
⊢ IsBigO (F := ℝ) atTop (f * g) fun (t : ℝ) ↦ t ^ c
have refine : ∀ᶠ (x : ℝ) in atTop, ‖x ^ a * x ^ b‖ ≤ x ^ c
Tactic: refine (hf.mul hg).trans (Eventually.isBigO ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : IsBigO (F := ℝ) atTop f fun (t : ℝ) ↦ t ^ a
hg : IsBigO (F := ℝ) atTop g fun (t : ℝ) ↦ t ^ b
h : a + b ≤ c
⊢ ∀ᶠ (x : ℝ) in atTop, ‖x ^ a * x ^ b‖ ≤ x ^ c
have h₁ : ∀ (t : ℝ) (ht : 1 ≤ t), ‖t ^ a * t ^ b‖ ≤ t ^ c
Tactic: filter_upwards [eventually_ge_atTop 1] with t ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : IsBigO (F := ℝ) atTop f fun (t : ℝ) ↦ t ^ a
hg : IsBigO (F := ℝ) atTop g fun (t : ℝ) ↦ t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ ‖t ^ a * t ^ b‖ ≤ t ^ c
have h₁ : t ^ (a + b) ≤ t ^ c
Tactic: rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) a
hg : IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) b
h : a + b ≤ c
⊢ IsBigO (F := ℝ) atTop (f * g) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) c
have refine : ∀ᶠ (x : ℕ) in atTop, ‖HPow.hPow (α := ℝ) (↑x : ℝ) a * HPow.hPow (α := ℝ) (↑x : ℝ) b‖ ≤ HPow.hPow (α := ℝ) (↑x : ℝ) c
Tactic: refine (hf.mul hg).trans (Eventually.isBigO ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) a
hg : IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) b
h : a + b ≤ c
⊢ ∀ᶠ (x : ℕ) in atTop, ‖HPow.hPow (α := ℝ) (↑x : ℝ) a * HPow.hPow (α := ℝ) (↑x : ℝ) b‖ ≤ HPow.hPow (α := ℝ) (↑x : ℝ) c
have h₁ : ∀ (t : ℕ) (ht : 1 ≤ t), ‖HPow.hPow (α := ℝ) (↑t : ℝ) a * HPow.hPow (α := ℝ) (↑t : ℝ) b‖ ≤ HPow.hPow (α := ℝ) (↑t : ℝ) c
Tactic: filter_upwards [eventually_ge_atTop 1] with t ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) a
hg : IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ t
⊢ ‖HPow.hPow (α := ℝ) (↑t : ℝ) a * HPow.hPow (α := ℝ) (↑t : ℝ) b‖ ≤ HPow.hPow (α := ℝ) (↑t : ℝ) c
have ht₁ : LE.le (α := ℝ) 1 (↑t : ℝ)
Tactic: replace ht : 1 ≤ (t : ℝ) := Nat.one_le_cast.mpr ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
E : Type u_2
inst : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) a
hg : IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) b
h : a + b ≤ c
t : ℕ
ht : LE.le (α := ℝ) 1 (↑t : ℝ)
⊢ ‖HPow.hPow (α := ℝ) (↑t : ℝ) a * HPow.hPow (α := ℝ) (↑t : ℝ) b‖ ≤ HPow.hPow (α := ℝ) (↑t : ℝ) c
have h₁ : HPow.hPow (α := ℝ) (↑t : ℝ) (a + b) ≤ HPow.hPow (α := ℝ) (↑t : ℝ) c
Tactic: rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
a : ℝ
ha : 0 < a
b : ℝ
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-a * x)) fun (x : ℝ) ↦ x ^ b
have hgf : ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0
Tactic: apply isLittleO_of_tendsto'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
a : ℝ
ha : 0 < a
b : ℝ
hgf : ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-a * x)) fun (x : ℝ) ↦ x ^ b
have a₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)
Tactic: apply isLittleO_of_tendsto'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0
have hgf : ∀ (t : ℝ) (ht : 0 < t) (h : t ^ b = 0), rexp (-a * t) = 0
Tactic: refine (eventually_gt_atTop 0).mono fun t ht h => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t ^ b = 0
⊢ rexp (-a * t) = 0
have h₁ : t = 0 ∧ b ≠ 0
Tactic: rw [rpow_eq_zero_iff_of_nonneg ht.le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)
have a₁ : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * x) / x ^ (-b))⁻¹ fun (x : ℝ) ↦ rexp (-a * x) / x ^ b
Tactic: refine (tendsto_exp_mul_div_rpow_atTop (-b) a ha).inv_tendsto_atTop.congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
a : ℝ
ha : 0 < a
b : ℝ
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * x) / x ^ (-b))⁻¹ fun (x : ℝ) ↦ rexp (-a * x) / x ^ b
have a₁ : ∀ (t : ℝ) (ht : 0 ≤ t),
  Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (a * x) / x ^ (-b))⁻¹ t) ((fun (x : ℝ) ↦ rexp (-a * x) / x ^ b) t)
Tactic: refine (eventually_ge_atTop 0).mono fun t ht => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
k a b : ℝ
ha' : a < b
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (a * t) * t ^ k) fun (t : ℝ) ↦ rexp (b * t)
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (a * x) * x ^ k / rexp (b * x)) atTop (𝓝 0)
Tactic: refine (isLittleO_of_tendsto (fun _ h ↦ (Real.exp_ne_zero _ h).elim) ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
k a b : ℝ
ha' : a < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (a * x) * x ^ k / rexp (b * x)) atTop (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k * rexp (-(b - a) * x)) atTop (𝓝 0)
Tactic: simp_rw [← div_mul_eq_mul_div₀, ← Real.exp_sub, ← sub_mul, ← neg_sub b a,
    mul_comm _ (_ ^ k)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
⊢ EventuallyLE (β := ℝ) atTop (fun (x : ℝ) ↦ ‖log x ^ r‖) fun (x : ℝ) ↦ log x ^ r'
have h : ∀ (x : ℝ) (hx : 1 ≤ log x), ‖log x ^ r‖ ≤ log x ^ r'
Tactic: filter_upwards [tendsto_log_atTop.eventually_ge_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ ‖log x ^ r‖ ≤ log x ^ r'
have h : log x ^ r ≤ log x ^ r'
Tactic: rw [Real.norm_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ log x ^ r ≤ log x ^ r'
have h : r ≤ r'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s r : ℝ
hs : s < 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (-s)) ∘ fun (x : ℝ) ↦ x⁻¹) x) ((fun (x : ℝ) ↦ x ^ s) x)
have rw : x⁻¹ ^ (-s) = (fun (x : ℝ) ↦ x ^ s) x
Tactic: rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s r : ℝ
hs : s < 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
rw : x⁻¹ ^ (-s) = (fun (x : ℝ) ↦ x ^ s) x
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (-s)) ∘ fun (x : ℝ) ↦ x⁻¹) x) ((fun (x : ℝ) ↦ x ^ s) x)
have rw₁ : (x ^ (-s))⁻¹ = (fun (x : ℝ) ↦ x ^ s) x
Tactic: rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s r : ℝ
hs : s < 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
rw : x⁻¹ ^ (-s) = (fun (x : ℝ) ↦ x ^ s) x
rw₁ : (x ^ (-s))⁻¹ = (fun (x : ℝ) ↦ x ^ s) x
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (-s)) ∘ fun (x : ℝ) ↦ x⁻¹) x) ((fun (x : ℝ) ↦ x ^ s) x)
have rw₂ : (x ^ s)⁻¹⁻¹ = (fun (x : ℝ) ↦ x ^ s) x
Tactic: rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
s r : ℝ
hs : s < 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
rw : x⁻¹ ^ (-s) = (fun (x : ℝ) ↦ x ^ s) x
rw₁ : (x ^ (-s))⁻¹ = (fun (x : ℝ) ↦ x ^ s) x
rw₂ : (x ^ s)⁻¹⁻¹ = (fun (x : ℝ) ↦ x ^ s) x
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (-s)) ∘ fun (x : ℝ) ↦ x⁻¹) x) ((fun (x : ℝ) ↦ x ^ s) x)
have rw₃ : x ^ s = (fun (x : ℝ) ↦ x ^ s) x
Tactic: rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
⊢ log x / x ^ (-r) = (fun (x : ℝ) ↦ log x * x ^ r) x
have rw : log x / (x ^ r)⁻¹ = (fun (x : ℝ) ↦ log x * x ^ r) x
Tactic: rw [rpow_neg hx.out.le, div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
rw : log x / (x ^ r)⁻¹ = (fun (x : ℝ) ↦ log x * x ^ r) x
⊢ log x / x ^ (-r) = (fun (x : ℝ) ↦ log x * x ^ r) x
have rw₁ : log x * x ^ r = (fun (x : ℝ) ↦ log x * x ^ r) x
Tactic: rw [rpow_neg hx.out.le, div_inv_eq_mul]