mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ 0 < b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (fun x ↦ b ^ x) atBot atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ 0 < b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ Tendsto (fun x ↦ b ^ x) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
⊢ |x ^ y| ≤ rexp (log x * y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ 0 ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ≠ -1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ 1 < b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ (log x)⁻¹ = rexp 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ Tendsto (fun x ↦ b ^ x) atBot (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto ?m.40 atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
this : (↑(θ.toReal + ψ.toReal)).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ x ^ (log x)⁻¹ ≤ rexp 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx_nonneg : 0 ≤ x
⊢ ‖x ^ y‖ = ‖x‖ ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y z : ℝ
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hψ : θ ≠ ↑π ∨ ψ ≠ ↑π
hs : θ.sign = -ψ.sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto (fun x ↦ x ^ (a / (b * x + c))) atTop (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: ⊢ Tendsto (fun x ↦ x ^ (1 / x)) atTop (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: ⊢ Tendsto (fun x ↦ x ^ (-1 / x)) atTop (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ x ^ w = x ^ y * x ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s : ℝ
⊢ Tendsto (fun x ↦ rexp x / x ^ s) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ rexp (b * x) / x ^ s) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s b : ℝ
hb : 0 < b
x : ℝ
⊢ (fun x ↦ rexp (b * x) / x ^ s)⁻¹ x = x ^ s * rexp (-b * x)

Tactic:
simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s b : ℝ
hb : 0 < b
x : ℝ
⊢ (fun x ↦ rexp (b * x) / x ^ s)⁻¹ x = x ^ s * rexp (-b * x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ x ^ s * rexp (-b * x)) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y * 0 ^ z ≤ 1 * 1

Tactic:
gcongr
          exacts [zero_rpow_nonneg z, zero_rpow_le_one y, zero_rpow_le_one z]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y * 0 ^ z ≤ 1 * 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 1 * 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : -(-θ).sign = (θ + ψ).sign
⊢ -θ ≠ ↑π

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
⊢ ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ Tendsto (fun x ↦ x ^ y) (𝓝 ∞) (𝓝 ∞)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
⊢ (θ + ψ).toReal ≤ 0 ∨ θ + ψ = ↑π

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h : ∀ x ∈ s, 0 ≤ f x
⊢ a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
⊢ x ^ (-y) = x⁻¹ ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ |(g x).im|
⊢ (fun x ↦ rexp ((f x).arg * (g x).im)) =Θ[l] fun x ↦ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ |(g x).im|
⊢ (have this := fun x ↦ ‖f x‖ ^ (g x).re / 1;
    this) =ᶠ[l]
    have this := fun x ↦ ‖f x‖ ^ (g x).re;
    this

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : (θ + ψ).toReal ≤ 0
⊢ 2 * π * ↑k ∈ Set.Ioo (2 * π * ↑(-1 - 1)) (2 * π * ↑(-1 + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : 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
⊢ (fun x ↦ ‖f x‖ ^ (g x).re / 1) =ᶠ[l] fun x ↦ ‖f x‖ ^ (g x).re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y z : ℝ
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
h : y - z ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(x ^ y) = ↑x ^ ↑y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
k : ℤ
hk : π - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : θ + ψ = ↑π
⊢ 2 * π * ↑k ∈ Set.Ioo (2 * π * ↑(0 - 1)) (2 * π * ↑(0 + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.sign = 1
hψs : ψ.sign = 1
hsa : (θ + ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
⊢ (-θ).sign = 1 ∧ (-ψ).sign = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : 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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : 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|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : 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 (c ^ r) l (fun x ↦ f x ^ r) fun x ↦ g x ^ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≤ 0
y : ℂ
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : 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 : α → ℝ},
    0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → f =Θ[l] g → r ≥ 0 → (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r
hr : ¬r ≥ 0
⊢ -r ≥ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
⊢ (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ (-θ + -ψ).sign ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
⊢ (fun x ↦ f x ^ r) =o[l] fun x ↦ g x ^ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =O[l] g
hg : 0 ≤ᶠ[l] g
⊢ (fun x ↦ √(f x)) =O[l] fun x ↦ √(g x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
⊢ ContinuousOn (sign ∘ f) s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =o[l] g
hg : 0 ≤ᶠ[l] g
⊢ (fun x ↦ √(f x)) =o[l] fun x ↦ √(g x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ (x ^ ↑y).re = ‖x‖ ^ y * Real.cos (x.arg * y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: 𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
n : ℕ
⊢ ‖g n / ↑(↑n ^ r)‖ = ((fun x ↦ ‖g x‖) / fun n ↦ ↑n ^ r) n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: 𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ g =O[atTop] fun n ↦ ↑n ^ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ (x ^ ↑y).im = ‖x‖ ^ y * Real.sin (x.arg * y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: z : ℂ
hz : z ≠ 0
w : ℂ
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
⊢ (f * g) =O[atTop] fun t ↦ t ^ c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n ↦ ↑n ^ a
hg : g =O[atTop] fun n ↦ ↑n ^ b
h : a + b ≤ c
⊢ (f * g) =O[atTop] fun n ↦ ↑n ^ c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: a b : ℝ
h : a ≤ b
himp : b = 0 → a = 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x ↦ ‖x ^ b‖ ≤ ‖x ^ a‖) x}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: a : ℝ
ha : a ≤ 1
⊢ 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: a : ℝ
ha : a ≤ 1
⊢ id =O[𝓝[≥] 0] fun x ↦ x ^ a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ x ^ s / rexp (b * x)) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: k : ℤ
b : ℝ
hb : 0 < b
⊢ (fun x ↦ x ^ k) =o[atTop] fun x ↦ rexp (b * x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: k : ℕ
b : ℝ
hb : 0 < b
⊢ (fun x ↦ x ^ k) =o[atTop] fun x ↦ rexp (b * x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s : ℝ
⊢ (fun x ↦ x ^ s) =o[atTop] rexp

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: z w : ℂ
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ ‖x ^ ↑y‖ = ‖x‖ ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x‖ ^ (↑n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x ↦ rexp (-a * x)) =o[atTop] fun x ↦ x ^ b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x‖ ^ (↑n)⁻¹

Tactic:
by
  rw [← norm_cpow_real]; simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℂ
⊢ ‖↑x ^ y‖ = x ^ y.re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: k a b : ℝ
ha' : a < b
⊢ (fun t ↦ rexp (a * t) * t ^ k) =o[atTop] fun t ↦ rexp (b * t)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖↑x ^ y‖ = x ^ y.re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ 0 ≤ log x ^ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: c : ℂ
⊢ (fun t ↦ ‖↑t ^ c‖) =ᶠ[atTop] fun t ↦ t ^ c.re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
s : ℂ
hs : s.re ≠ 0
⊢ ‖↑n ^ s‖ = ↑n ^ s.re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℂ
⊢ ‖↑n ^ s‖ = ↑n ^ s.re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
⊢ (fun x ↦ ‖log x ^ r‖) ≤ᶠ[atTop] fun x ↦ log x ^ r'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 0 ≤ x
⊢ (fun x ↦ (x ^ (s / r')) ^ r') x = (fun x ↦ x ^ s) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x ↦ ((fun x ↦ log x ^ r) ∘ fun x ↦ x⁻¹) x = (fun x ↦ |log x| ^ r) x) x}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((fun x ↦ x ^ (-s)) ∘ fun x ↦ x⁻¹) x = (fun x ↦ x ^ s) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: r : ℝ
hr : r < 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x ↦ (fun x ↦ -|log x| ^ 1) x = log x) x}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ ↑x ^ (↑y * z) = ↑(x ^ y) ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ log x / x ^ (-r) = (fun x ↦ log x * x ^ r) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
⊢ ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) x = log x * x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ n) ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
⊢ (x ^ y) ^ n = (x ^ n) ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: ⊢ Tendsto (fun x ↦ log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst✝³ : SMul M α
inst✝² : SMul N β
inst✝¹ : FunLike F α β
inst✝ : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective fun m ↦ c • m
hc' : Injective fun n ↦ σ c • n
⊢ ⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y + ↑n ≠ 0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y + ↑n ≠ 0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y - ↑n ≠ 0
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y - ↑n ≠ 0
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
⊢ x ^ (1 + y) = x * x ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : y - 1 ≠ 0
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : 1 - y ≠ 0
⊢ x ^ (1 - y) = x / x ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ x ^ 2 = x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ x ^ (-1) = x⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
⊢ 0 < x ^ 0

Tactic:
by

Goal state after: