awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ |(g x).im|
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
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ rexp ((f x).arg * (g x).im)) fun (x : α) ↦ 1

Tactic:
rcases hl with ⟨b, hb⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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

Tactic:
Real.isTheta_exp_comp_one.2 ⟨π * b, ?_⟩

Premises used: Iff.mpr, Real.pi, HMul.hMul, Real.isTheta_exp_comp_one, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
refine : ∀ᶠ (x : ℝ) in Filter.map (fun (x : α) ↦ |(f x).arg * (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:
refine Real.isTheta_exp_comp_one.2 ⟨π * b, ?_⟩

Premises used: Iff.mpr, Real.pi, HMul.hMul, Real.isTheta_exp_comp_one, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
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)
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun (x : α) ↦ |(f x).arg * (g x).im|) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (π * b)

Tactic:
rw [eventually_map] at hb ⊢

Premises used: Filter.eventually_map
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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)

Tactic:
hb.mono fun x hx => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(g a).im| b
refine :
  ∀ (x : α) (hx : (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(g x).im| b), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(f x).arg * (g x).im| (π * b)
⊢ ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(f a).arg * (g a).im| (π * b)

Tactic:
refine hb.mono fun x hx => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
rw : |(f x).arg| * |(g x).im| ≤ π * b
⊢ (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) |(f x).arg * (g x).im| (π * b)

Tactic:
rw [abs_mul]

Premises used: abs_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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)

Tactic:
mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) Real.pi_pos.le

Premises used: Complex.abs_arg_le_pi, Real.pi_pos, LT.lt.le, mul_le_mul, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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)

Tactic:
exact mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) Real.pi_pos.le

Premises used: Complex.abs_arg_le_pi, Real.pi_pos, LT.lt.le, mul_le_mul, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ |(g x).im|
⊢ l.EventuallyEq (β := ℝ)
    (have this : α → ℝ := fun (x : α) ↦ ‖f x‖ ^ (g x).re / 1;
    this)
    (have this : α → ℝ := fun (x : α) ↦ ‖f x‖ ^ (g x).re;
    this)

Tactic:
simp only [div_one, EventuallyEq.rfl]

Premises used: Filter.EventuallyEq.rfl, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
hl_im : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ |(g x).im|
hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0
⊢ l.EventuallyEq (β := ℝ) (fun (x : α) ↦ ‖f x‖ ^ (g x).re / 1) fun (x : α) ↦ ‖f x‖ ^ (g x).re

Tactic:
simp only [div_one, EventuallyEq.rfl]

Premises used: Filter.EventuallyEq.rfl, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ ∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0

Tactic:
simpa only [eventually_imp_distrib_right, not_imp_not, Imp.swap (a := b.re = 0)] using hl

Premises used: Filter.eventually_imp_distrib_right, Imp.swap, not_imp_not
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
a : ∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
⊢ IsBigOWith (E := ℝ) (F := ℝ) (c ^ r) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r

Tactic:
apply IsBigOWith.of_bound

Premises used: Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
h₁ : ∀ (x : α) (hgx : 0 x ≤ g x) (hx : ‖f x‖ ≤ c * ‖g x‖), ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
⊢ ∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖

Tactic:
filter_upwards [hg, h.bound] with x hgx hx

Premises used: Asymptotics.IsBigOWith.bound
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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| ≤ |f x| ^ r

Tactic:
abs_rpow_le_abs_rpow _ _

Premises used: Real.abs_rpow_le_abs_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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‖
h₁ : |f x| ≤ c * |g x|
⊢ |f x| ^ r ≤ (c * |g x|) ^ r

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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| ≤ c * |g x|

Tactic:
assumption
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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|
rw₁ rw₂ : c ^ r * |g x| ^ r = c ^ r * |g x| ^ r
⊢ (c * |g x|) ^ r = c ^ r * |g x ^ r|

Tactic:
rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]

Premises used: Real.mul_rpow, Real.abs_rpow_of_nonneg, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
x₂ : (c * |g x|) ^ r = c ^ r * |g x ^ r|
⊢ ‖f 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]

Premises used: HMul.hMul, abs, Real.abs_rpow_le_abs_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
h : f =O[l] g
⊢ IsBigO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r

Tactic:
let ⟨_, hc, h'⟩ := h.exists_nonneg
  (h'.rpow hc hr hg).isBigO

Premises used: Asymptotics.IsBigO, Asymptotics.IsBigOWith.rpow, Asymptotics.IsBigO.exists_nonneg, HPow.hPow, Asymptotics.IsBigOWith.isBigO, _private.0.Asymptotics.IsBigO.rpow.match_1
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
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
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r

Tactic:
wlog hr : r ≥ 0 with rpow_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
inr : 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

Tactic:
rw [← isTheta_inv]

Premises used: Asymptotics.isTheta_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
inr : 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)⁻¹

Tactic:
grw [← EventuallyEq.isTheta <| hf.mono fun x hfx ↦ Real.rpow_neg hfx r]

Premises used: Filter.EventuallyEq.isTheta, Filter.Eventually.mono, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
inr : 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)⁻¹

Tactic:
grw [← EventuallyEq.isTheta <| hg.mono fun x hgx ↦ Real.rpow_neg hgx r]

Premises used: Filter.EventuallyEq.isTheta, Filter.Eventually.mono, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
linarith : -r < 0 → r - 0 + (-r - 0) = 0
⊢ -r ≥ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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)

Tactic:
exact rpow_pos hf hg h <| by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α_1 : Type u_1
r_1 : ℝ
l_1 : Filter α_1
f_1 g_1 : α_1 → ℝ
α : 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:
⟨h.1.rpow hr hg, h.2.rpow hr hf⟩

Premises used: Asymptotics.IsTheta, And.right, And.left, And.intro, Asymptotics.IsBigO.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α_1 : Type u_1
r_1 : ℝ
l_1 : Filter α_1
f_1 g_1 : α_1 → ℝ
α : 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:
exact ⟨h.1.rpow hr hg, h.2.rpow hr hf⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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

Tactic:
.of_isBigOWith fun c hc ↦ ?_

Premises used: Asymptotics.IsLittleO.of_isBigOWith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
refine : ∀ (c : ℝ) (hc : 0 < c), IsBigOWith (E := ℝ) (F := ℝ) c l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r

Tactic:
refine .of_isBigOWith fun c hc ↦ ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
rw : IsBigOWith (E := ℝ) (F := ℝ) ((c ^ r⁻¹) ^ r) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r
⊢ IsBigOWith (E := ℝ) (F := ℝ) c l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r

Tactic:
rw [← rpow_inv_rpow hc.le hr.ne']

Premises used: LT.lt.le, LT.lt.ne', Real.rpow_inv_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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

Tactic:
(h.forall_isBigOWith ?_).rpow ?_ ?_ hg

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsBigOWith.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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⁻¹
refine_3 : 0 ≤ r
⊢ IsBigOWith (E := ℝ) (F := ℝ) ((c ^ r⁻¹) ^ r) l (fun (x : α) ↦ f x ^ r) fun (x : α) ↦ g x ^ r

Tactic:
refine (h.forall_isBigOWith ?_).rpow ?_ ?_ hg

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsBigOWith.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
⊢ 0 < c ^ r⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
⊢ 0 ≤ c ^ r⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
⊢ 0 ≤ r

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =O[l] g
hg : 0 ≤ᶠ[l] g
⊢ IsBigO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ √(f x)) fun (x : α) ↦ √(g x)

Tactic:
simpa [Real.sqrt_eq_rpow] using hfg.rpow one_half_pos.le hg

Premises used: LT.lt.le, one_half_pos, Asymptotics.IsBigO.rpow, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =o[l] g
hg : 0 ≤ᶠ[l] g
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ √(f x)) fun (x : α) ↦ √(g x)

Tactic:
simpa [Real.sqrt_eq_rpow] using hfg.rpow one_half_pos hg

Premises used: Asymptotics.IsLittleO.rpow, one_half_pos, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =Θ[l] g
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
⊢ IsTheta (E := ℝ) (F := ℝ) l (fun (x : α) ↦ √(f x)) fun (x : α) ↦ √(g x)

Tactic:
⟨hfg.1.sqrt hg, hfg.2.sqrt hf⟩

Premises used: Asymptotics.IsTheta, Asymptotics.IsBigO.sqrt, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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

Tactic:
(isBigO_of_div_tendsto_nhds ?_ ‖a‖ ?_).of_norm_left

Premises used: Norm.norm, Asymptotics.isBigO_of_div_tendsto_nhds, Asymptotics.IsBigO.of_norm_left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
refine_2 :
  Tendsto (HDiv.hDiv (α := ℕ → ℝ) (fun (x : ℕ) ↦ ‖g x‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r) atTop (𝓝 ‖a‖)
⊢ IsBigO (F := ℝ) atTop g fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r

Tactic:
refine (isBigO_of_div_tendsto_nhds ?_ ‖a‖ ?_).of_norm_left

Premises used: Norm.norm, Asymptotics.isBigO_of_div_tendsto_nhds, Asymptotics.IsBigO.of_norm_left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun (n : ℕ) ↦ g n / (↑(HPow.hPow (α := ℝ) (↑n : ℝ) r) : 𝕜)) atTop (𝓝 a)
h : ∀ (a : ℕ) (h : a ≠ 0), HPow.hPow (α := ℝ) (↑a : ℝ) r = 0 → ‖g a‖ = 0
⊢ ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := ℝ) (↑x : ℝ) r = 0 → ‖g x‖ = 0

Tactic:
filter_upwards [eventually_ne_atTop 0] with _ h

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun (n : ℕ) ↦ g n / (↑(HPow.hPow (α := ℝ) (↑n : ℝ) r) : 𝕜)) atTop (𝓝 a)
a_1 : ℕ
h : a_1 ≠ 0
⊢ HPow.hPow (α := ℝ) (↑a_1 : ℝ) r = 0 → ‖g a_1‖ = 0

Tactic:
simp [Real.rpow_eq_zero_iff_of_nonneg, h]

Premises used: Real.rpow_eq_zero_iff_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun (n : ℕ) ↦ g n / (↑(HPow.hPow (α := ℝ) (↑n : ℝ) r) : 𝕜)) atTop (𝓝 a)
n : ℕ
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑n : ℝ) r

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun (n : ℕ) ↦ g n / (↑(HPow.hPow (α := ℝ) (↑n : ℝ) r) : 𝕜)) atTop (𝓝 a)
n : ℕ
⊢ ‖g n / (↑(HPow.hPow (α := ℝ) (↑n : ℝ) r) : 𝕜)‖ =
    HDiv.hDiv (α := ℕ → ℝ) (β := ℕ → ℝ) (fun (x : ℕ) ↦ ‖g x‖) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r) n

Tactic:
simp [abs_of_nonneg, show 0 ≤ (n : ℝ) ^ r by positivity]

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun (n : ℕ) ↦ g n / (↑(HPow.hPow (α := ℝ) (↑n : ℝ) r) : 𝕜)) atTop (𝓝 a)
⊢ Tendsto (HDiv.hDiv (α := ℕ → ℝ) (fun (x : ℕ) ↦ ‖g x‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r) atTop (𝓝 ‖a‖)

Tactic:
exact hlim.norm.congr fun n ↦ by simp [abs_of_nonneg, show 0 ≤ (n : ℝ) ^ r by positivity]

Premises used: Filter.Tendsto.norm, Filter.Tendsto.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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

Tactic:
(hf.mul hg).trans (Eventually.isBigO ?_)

Premises used: Asymptotics.IsBigO.mul, Asymptotics.IsBigO.trans, Filter.Eventually.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
refine : ∀ᶠ (x : ℝ) in atTop, ‖x ^ a * x ^ b‖ ≤ x ^ c
⊢ IsBigO (F := ℝ) atTop (f * g) fun (t : ℝ) ↦ t ^ c

Tactic:
refine (hf.mul hg).trans (Eventually.isBigO ?_)

Premises used: Asymptotics.IsBigO.mul, Asymptotics.IsBigO.trans, Filter.Eventually.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
h₁ : ∀ (t : ℝ) (ht : 1 ≤ t), ‖t ^ a * t ^ b‖ ≤ t ^ c
⊢ ∀ᶠ (x : ℝ) in atTop, ‖x ^ a * x ^ b‖ ≤ x ^ c

Tactic:
filter_upwards [eventually_ge_atTop 1] with t ht

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
h₁ : t ^ (a + b) ≤ t ^ c
⊢ ‖t ^ a * t ^ 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))]

Premises used: zero_le_one, zero_lt_one, HAdd.hAdd, LT.lt.trans_le, Real.rpow_add, Real.rpow_nonneg, LE.le.trans, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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 + b) ≤ t ^ c

Tactic:
Real.rpow_le_rpow_of_exponent_le ht h

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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 + b) ≤ t ^ c

Tactic:
exact Real.rpow_le_rpow_of_exponent_le ht h

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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

Tactic:
(hf.mul hg).trans (Eventually.isBigO ?_)

Premises used: Asymptotics.IsBigO.mul, Asymptotics.IsBigO.trans, Filter.Eventually.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
refine :
  ∀ᶠ (x : ℕ) in atTop, ‖HPow.hPow (α := ℝ) (↑x : ℝ) a * HPow.hPow (α := ℝ) (↑x : ℝ) b‖ ≤ HPow.hPow (α := ℝ) (↑x : ℝ) c
⊢ IsBigO (F := ℝ) atTop (f * g) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) c

Tactic:
refine (hf.mul hg).trans (Eventually.isBigO ?_)

Premises used: Asymptotics.IsBigO.mul, Asymptotics.IsBigO.trans, Filter.Eventually.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
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
h₁ :
  ∀ (t : ℕ) (ht : 1 ≤ t),
    ‖HPow.hPow (α := ℝ) (↑t : ℝ) a * HPow.hPow (α := ℝ) (↑t : ℝ) b‖ ≤ HPow.hPow (α := ℝ) (↑t : ℝ) c
⊢ ∀ᶠ (x : ℕ) in atTop, ‖HPow.hPow (α := ℝ) (↑x : ℝ) a * HPow.hPow (α := ℝ) (↑x : ℝ) b‖ ≤ HPow.hPow (α := ℝ) (↑x : ℝ) c

Tactic:
filter_upwards [eventually_ge_atTop 1] with t ht

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat