[GOAL]
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => x ^ y) atTop atTop
[PROOFSTEP]
rw [tendsto_atTop_atTop]
[GOAL]
y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y
[PROOFSTEP]
intro b
[GOAL]
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y
[PROOFSTEP]
use max b 0 ^ (1 / y)
[GOAL]
case h
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∀ (a : ℝ), max b 0 ^ (1 / y) ≤ a → b ≤ a ^ y
[PROOFSTEP]
intro x hx
[GOAL]
case h
y : ℝ
hy : 0 < y
b x : ℝ
hx : max b 0 ^ (1 / y) ≤ x
⊢ b ≤ x ^ y
[PROOFSTEP]
exact
  le_of_max_le_left
    (by
      convert rpow_le_rpow (rpow_nonneg_of_nonneg (le_max_right b 0) (1 / y)) hx (le_of_lt hy) using 1
      rw [← rpow_mul (le_max_right b 0), (eq_div_iff (ne_of_gt hy)).mp rfl, Real.rpow_one])
[GOAL]
y : ℝ
hy : 0 < y
b x : ℝ
hx : max b 0 ^ (1 / y) ≤ x
⊢ max b ?m.773 ≤ x ^ y
[PROOFSTEP]
convert rpow_le_rpow (rpow_nonneg_of_nonneg (le_max_right b 0) (1 / y)) hx (le_of_lt hy) using 1
[GOAL]
case h.e'_3
y : ℝ
hy : 0 < y
b x : ℝ
hx : max b 0 ^ (1 / y) ≤ x
⊢ max b ?m.773 = (max b 0 ^ (1 / y)) ^ y
[PROOFSTEP]
rw [← rpow_mul (le_max_right b 0), (eq_div_iff (ne_of_gt hy)).mp rfl, Real.rpow_one]
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
⊢ Tendsto (Real.rpow b) atTop (𝓝 0)
[PROOFSTEP]
show Tendsto (fun z => b ^ z) atTop (𝓝 0)
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
⊢ Tendsto (fun z => b ^ z) atTop (𝓝 0)
[PROOFSTEP]
rcases lt_trichotomy b 0 with hb | rfl | hb
[GOAL]
case inl
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun z => b ^ z) atTop (𝓝 0)
case inr.inl
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun z => 0 ^ z) atTop (𝓝 0)
case inr.inr b : ℝ hb₀ : -1 < b hb₁ : b < 1 hb : 0 < b ⊢ Tendsto (fun z => b ^ z) atTop (𝓝 0)
[PROOFSTEP]
case inl =>
  -- b < 0
  simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
  rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
  refine IsLittleO.mul_isBigO ?exp ?cos
  case exp =>
    rw [isLittleO_const_iff one_ne_zero]
    refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
    rw [← log_neg_eq_log, log_neg_iff (by linarith)]
    linarith
  case cos =>
    rw [isBigO_iff]
    exact ⟨1, eventually_of_forall fun x => by simp [Real.abs_cos_le_one]⟩
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun z => b ^ z) atTop (𝓝 0)
[PROOFSTEP]
case inl =>
  -- b < 0
  simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
  rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
  refine IsLittleO.mul_isBigO ?exp ?cos
  case exp =>
    rw [isLittleO_const_iff one_ne_zero]
    refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
    rw [← log_neg_eq_log, log_neg_iff (by linarith)]
    linarith
  case cos =>
    rw [isBigO_iff]
    exact ⟨1, eventually_of_forall fun x => by simp [Real.abs_cos_le_one]⟩
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun z => b ^ z) atTop (𝓝 0)
[PROOFSTEP]
simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun z => exp (log b * z) * cos (z * π)) atTop (𝓝 0)
[PROOFSTEP]
rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun z => exp (log b * z) * cos (z * π)) =o[atTop] fun _x => 1 * 1
[PROOFSTEP]
refine IsLittleO.mul_isBigO ?exp ?cos
[GOAL]
case exp
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun z => exp (log b * z)) =o[atTop] fun _x => 1
case cos b : ℝ hb₀ : -1 < b hb₁ : b < 1 hb : b < 0 ⊢ (fun z => cos (z * π)) =O[atTop] fun _x => 1
[PROOFSTEP]
case exp =>
  rw [isLittleO_const_iff one_ne_zero]
  refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
  rw [← log_neg_eq_log, log_neg_iff (by linarith)]
  linarith
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun z => exp (log b * z)) =o[atTop] fun _x => 1
[PROOFSTEP]
case exp =>
  rw [isLittleO_const_iff one_ne_zero]
  refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
  rw [← log_neg_eq_log, log_neg_iff (by linarith)]
  linarith
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun z => exp (log b * z)) =o[atTop] fun _x => 1
[PROOFSTEP]
rw [isLittleO_const_iff one_ne_zero]
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun z => exp (log b * z)) atTop (𝓝 0)
[PROOFSTEP]
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ log b < 0
[PROOFSTEP]
rw [← log_neg_eq_log, log_neg_iff (by linarith)]
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ 0 < -b
[PROOFSTEP]
linarith
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ -b < 1
[PROOFSTEP]
linarith
[GOAL]
case cos
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun z => cos (z * π)) =O[atTop] fun _x => 1
[PROOFSTEP]
case cos =>
  rw [isBigO_iff]
  exact ⟨1, eventually_of_forall fun x => by simp [Real.abs_cos_le_one]⟩
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun z => cos (z * π)) =O[atTop] fun _x => 1
[PROOFSTEP]
case cos =>
  rw [isBigO_iff]
  exact ⟨1, eventually_of_forall fun x => by simp [Real.abs_cos_le_one]⟩
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun z => cos (z * π)) =O[atTop] fun _x => 1
[PROOFSTEP]
rw [isBigO_iff]
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, ‖cos (x * π)‖ ≤ c * ‖1‖
[PROOFSTEP]
exact ⟨1, eventually_of_forall fun x => by simp [Real.abs_cos_le_one]⟩
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
x : ℝ
⊢ ‖cos (x * π)‖ ≤ 1 * ‖1‖
[PROOFSTEP]
simp [Real.abs_cos_le_one]
[GOAL]
case inr.inl
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun z => 0 ^ z) atTop (𝓝 0)
case inr.inr b : ℝ hb₀ : -1 < b hb₁ : b < 1 hb : 0 < b ⊢ Tendsto (fun z => b ^ z) atTop (𝓝 0)
[PROOFSTEP]
case inr.inl =>
  -- b = 0
  refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
  rw [tendsto_pure]
  filter_upwards [eventually_ne_atTop 0] with _ hx
  simp [hx]
[GOAL]
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun z => 0 ^ z) atTop (𝓝 0)
[PROOFSTEP]
case inr.inl =>
  -- b = 0
  refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
  rw [tendsto_pure]
  filter_upwards [eventually_ne_atTop 0] with _ hx
  simp [hx]
[GOAL]
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun z => 0 ^ z) atTop (𝓝 0)
[PROOFSTEP]
refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
[GOAL]
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun z => 0 ^ z) atTop (pure 0)
[PROOFSTEP]
rw [tendsto_pure]
[GOAL]
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ^ x = 0
[PROOFSTEP]
filter_upwards [eventually_ne_atTop 0] with _ hx
[GOAL]
case h
hb₀ : -1 < 0
hb₁ : 0 < 1
a✝ : ℝ
hx : a✝ ≠ 0
⊢ 0 ^ a✝ = 0
[PROOFSTEP]
simp [hx]
[GOAL]
case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun z => b ^ z) atTop (𝓝 0)
[PROOFSTEP]
case inr.inr =>
  -- b > 0
  simp_rw [Real.rpow_def_of_pos hb]
  refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
  exact (log_neg_iff hb).mpr hb₁
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun z => b ^ z) atTop (𝓝 0)
[PROOFSTEP]
case inr.inr =>
  -- b > 0
  simp_rw [Real.rpow_def_of_pos hb]
  refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
  exact (log_neg_iff hb).mpr hb₁
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun z => b ^ z) atTop (𝓝 0)
[PROOFSTEP]
simp_rw [Real.rpow_def_of_pos hb]
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun z => exp (log b * z)) atTop (𝓝 0)
[PROOFSTEP]
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
[GOAL]
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ log b < 0
[PROOFSTEP]
exact (log_neg_iff hb).mpr hb₁
[GOAL]
b : ℝ
hb : 1 < b
⊢ Tendsto (Real.rpow b) atBot (𝓝 0)
[PROOFSTEP]
show Tendsto (fun z => b ^ z) atBot (nhds 0)
[GOAL]
b : ℝ
hb : 1 < b
⊢ Tendsto (fun z => b ^ z) atBot (𝓝 0)
[PROOFSTEP]
simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
[GOAL]
b : ℝ
hb : 1 < b
⊢ 0 < b
[PROOFSTEP]
positivity
[GOAL]
b : ℝ
hb : 1 < b
⊢ Tendsto (fun z => exp (log b * z)) atBot (𝓝 0)
[PROOFSTEP]
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_pos ?_).mpr tendsto_id
[GOAL]
b : ℝ
hb : 1 < b
⊢ 0 < log b
[PROOFSTEP]
exact (log_pos_iff (by positivity)).mpr <| by aesop
[GOAL]
b : ℝ
hb : 1 < b
⊢ 0 < b
[PROOFSTEP]
positivity
[GOAL]
b : ℝ
hb : 1 < b
⊢ 1 < b
[PROOFSTEP]
aesop
[GOAL]
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (Real.rpow b) atBot atTop
[PROOFSTEP]
show Tendsto (fun z => b ^ z) atBot atTop
[GOAL]
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (fun z => b ^ z) atBot atTop
[PROOFSTEP]
simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
[GOAL]
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ 0 < b
[PROOFSTEP]
positivity
[GOAL]
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (fun z => exp (log b * z)) atBot atTop
[PROOFSTEP]
refine tendsto_exp_atTop.comp <| (tendsto_const_mul_atTop_iff_neg <| tendsto_id (α := ℝ)).mpr ?_
[GOAL]
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ log b < 0
[PROOFSTEP]
exact (log_neg_iff hb₀).mpr hb₁
[GOAL]
b : ℝ
hb : 1 < b
⊢ Tendsto (Real.rpow b) atBot (𝓝 0)
[PROOFSTEP]
show Tendsto (fun z => b ^ z) atBot (𝓝 0)
[GOAL]
b : ℝ
hb : 1 < b
⊢ Tendsto (fun z => b ^ z) atBot (𝓝 0)
[PROOFSTEP]
simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
[GOAL]
b : ℝ
hb : 1 < b
⊢ 0 < b
[PROOFSTEP]
positivity
[GOAL]
b : ℝ
hb : 1 < b
⊢ Tendsto (fun z => exp (log b * z)) atBot (𝓝 0)
[PROOFSTEP]
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_iff_pos <| tendsto_id (α := ℝ)).mpr ?_
[GOAL]
b : ℝ
hb : 1 < b
⊢ 0 < log b
[PROOFSTEP]
exact (log_pos_iff (by positivity)).mpr <| by aesop
[GOAL]
b : ℝ
hb : 1 < b
⊢ 0 < b
[PROOFSTEP]
positivity
[GOAL]
b : ℝ
hb : 1 < b
⊢ 1 < b
[PROOFSTEP]
aesop
[GOAL]
a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto (fun x => x ^ (a / (b * x + c))) atTop (𝓝 1)
[PROOFSTEP]
refine'
  Tendsto.congr' _
    ((tendsto_exp_nhds_0_nhds_1.comp
          (by
            simpa only [mul_zero, pow_one] using
              (@tendsto_const_nhds _ _ _ a _).mul (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp
      tendsto_log_atTop)
[GOAL]
a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto ?m.296219 atTop (𝓝 0)
[PROOFSTEP]
simpa only [mul_zero, pow_one] using (@tendsto_const_nhds _ _ _ a _).mul (tendsto_div_pow_mul_exp_add_atTop b c 1 hb)
[GOAL]
a b c : ℝ
hb : 0 ≠ b
⊢ (exp ∘ fun x => a * (x / (b * exp x + c))) ∘ log =ᶠ[atTop] fun x => x ^ (a / (b * x + c))
[PROOFSTEP]
apply eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ))
[GOAL]
a b c : ℝ
hb : 0 ≠ b
⊢ EqOn ((exp ∘ fun x => a * (x / (b * exp x + c))) ∘ log) (fun x => x ^ (a / (b * x + c))) (Set.Ioi 0)
[PROOFSTEP]
intro x hx
[GOAL]
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((exp ∘ fun x => a * (x / (b * exp x + c))) ∘ log) x = (fun x => x ^ (a / (b * x + c))) x
[PROOFSTEP]
simp only [Set.mem_Ioi, Function.comp_apply] at hx ⊢
[GOAL]
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ exp (a * (log x / (b * exp (log x) + c))) = x ^ (a / (b * x + c))
[PROOFSTEP]
rw [exp_log hx, ← exp_log (rpow_pos_of_pos hx (a / (b * x + c))), log_rpow hx (a / (b * x + c))]
[GOAL]
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ exp (a * (log x / (b * x + c))) = exp (a / (b * x + c) * log x)
[PROOFSTEP]
field_simp
[GOAL]
⊢ Tendsto (fun x => x ^ (1 / x)) atTop (𝓝 1)
[PROOFSTEP]
convert tendsto_rpow_div_mul_add (1 : ℝ) _ (0 : ℝ) zero_ne_one
[GOAL]
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0
[PROOFSTEP]
funext
[GOAL]
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0
[PROOFSTEP]
ring
[GOAL]
⊢ Tendsto (fun x => x ^ (-1 / x)) atTop (𝓝 1)
[PROOFSTEP]
convert tendsto_rpow_div_mul_add (-(1 : ℝ)) _ (0 : ℝ) zero_ne_one
[GOAL]
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0
[PROOFSTEP]
funext
[GOAL]
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0
[PROOFSTEP]
ring
[GOAL]
s : ℝ
⊢ Tendsto (fun x => exp x / x ^ s) atTop atTop
[PROOFSTEP]
cases' archimedean_iff_nat_lt.1 Real.instArchimedean s with n hn
[GOAL]
case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ Tendsto (fun x => exp x / x ^ s) atTop atTop
[PROOFSTEP]
refine' tendsto_atTop_mono' _ _ (tendsto_exp_div_pow_atTop n)
[GOAL]
case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ (fun x => exp x / x ^ n) ≤ᶠ[atTop] fun x => exp x / x ^ s
[PROOFSTEP]
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_ge_atTop (1 : ℝ)] with x hx₀ hx₁
[GOAL]
case h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ exp x / x ^ n ≤ exp x / x ^ s
[PROOFSTEP]
rw [div_le_div_left (exp_pos _) (pow_pos hx₀ _) (rpow_pos_of_pos hx₀ _), ← Real.rpow_nat_cast]
[GOAL]
case h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ ↑n
[PROOFSTEP]
exact rpow_le_rpow_of_exponent_le hx₁ hn.le
[GOAL]
s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => exp (b * x) / x ^ s) atTop atTop
[PROOFSTEP]
refine' ((tendsto_rpow_atTop hb).comp (tendsto_exp_div_rpow_atTop (s / b))).congr' _
[GOAL]
s b : ℝ
hb : 0 < b
⊢ ((fun x => x ^ b) ∘ fun x => exp x / x ^ (s / b)) =ᶠ[atTop] fun x => exp (b * x) / x ^ s
[PROOFSTEP]
filter_upwards [eventually_ge_atTop (0 : ℝ)] with x hx₀
[GOAL]
case h
s b : ℝ
hb : 0 < b
x : ℝ
hx₀ : 0 ≤ x
⊢ ((fun x => x ^ b) ∘ fun x => exp x / x ^ (s / b)) x = exp (b * x) / x ^ s
[PROOFSTEP]
simp [Real.div_rpow, (exp_pos x).le, rpow_nonneg_of_nonneg, ← Real.rpow_mul, ← exp_mul, mul_comm x, hb.ne', *]
[GOAL]
s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => x ^ s * exp (-b * x)) atTop (𝓝 0)
[PROOFSTEP]
refine' (tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' _
[GOAL]
s b : ℝ
hb : 0 < b
⊢ (fun x => exp (b * x) / x ^ s)⁻¹ =ᶠ[atTop] fun x => x ^ s * exp (-b * x)
[PROOFSTEP]
filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]
[GOAL]
s b : ℝ
hb : 0 < b
x : ℝ
⊢ (fun x => exp (b * x) / x ^ s)⁻¹ x = x ^ s * exp (-b * x)
[PROOFSTEP]
simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]
[GOAL]
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => ↑x ^ y) atTop atTop
[PROOFSTEP]
rw [Filter.tendsto_atTop_atTop]
[GOAL]
y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ ↑a ^ y
[PROOFSTEP]
intro b
[GOAL]
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ ↑a ^ y
[PROOFSTEP]
obtain ⟨c, hc⟩ := tendsto_atTop_atTop.mp (tendsto_rpow_atTop hy) b
[GOAL]
case intro
y : ℝ
hy : 0 < y
b c : ℝ
hc : ∀ (a : ℝ), c ≤ a → b ≤ a ^ y
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ ↑a ^ y
[PROOFSTEP]
use c.toNNReal
[GOAL]
case h
y : ℝ
hy : 0 < y
b c : ℝ
hc : ∀ (a : ℝ), c ≤ a → b ≤ a ^ y
⊢ ∀ (a : ℝ≥0), toNNReal c ≤ a → b ≤ ↑a ^ y
[PROOFSTEP]
intro a ha
[GOAL]
case h
y : ℝ
hy : 0 < y
b c : ℝ
hc : ∀ (a : ℝ), c ≤ a → b ≤ a ^ y
a : ℝ≥0
ha : toNNReal c ≤ a
⊢ b ≤ ↑a ^ y
[PROOFSTEP]
exact_mod_cast hc a (Real.toNNReal_le_iff_le_coe.mp ha)
[GOAL]
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => x ^ y) (𝓝 ⊤) (𝓝 ⊤)
[PROOFSTEP]
rw [ENNReal.tendsto_nhds_top_iff_nnreal]
[GOAL]
y : ℝ
hy : 0 < y
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
[PROOFSTEP]
intro x
[GOAL]
y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
[PROOFSTEP]
obtain ⟨c, _, hc⟩ := (atTop_basis_Ioi.tendsto_iff atTop_basis_Ioi).mp (NNReal.tendsto_rpow_atTop hy) x trivial
[GOAL]
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
[PROOFSTEP]
have hc' : Set.Ioi ↑c ∈ 𝓝 (⊤ : ℝ≥0∞) := Ioi_mem_nhds ENNReal.coe_lt_top
[GOAL]
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
[PROOFSTEP]
refine' eventually_of_mem hc' _
[GOAL]
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
⊢ ∀ (x_1 : ℝ≥0∞), x_1 ∈ Set.Ioi ↑c → ↑x < x_1 ^ y
[PROOFSTEP]
intro a ha
[GOAL]
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
⊢ ↑x < a ^ y
[PROOFSTEP]
by_cases ha' : a = ⊤
[GOAL]
case pos
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
ha' : a = ⊤
⊢ ↑x < a ^ y
[PROOFSTEP]
simp [ha', hy]
[GOAL]
case neg
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
ha' : ¬a = ⊤
⊢ ↑x < a ^ y
[PROOFSTEP]
lift a to ℝ≥0 using ha'
[GOAL]
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0
ha : ↑a ∈ Set.Ioi ↑c
⊢ ↑x < ↑a ^ y
[PROOFSTEP]
simp only [Set.mem_Ioi, coe_lt_coe] at ha hc 
[GOAL]
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → ↑x < ↑x_1 ^ y
⊢ ↑x < ↑a ^ y
[PROOFSTEP]
rw [ENNReal.coe_rpow_of_nonneg _ hy.le]
[GOAL]
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → ↑x < ↑x_1 ^ y
⊢ ↑x < ↑(a ^ y)
[PROOFSTEP]
exact_mod_cast hc a ha
[GOAL]
α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|
⊢ (fun x => Real.exp (arg (f x) * (g x).im)) =Θ[l] fun x => 1
[PROOFSTEP]
rcases hl with ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => |(g x).im|) l, (fun x x_1 => x ≤ x_1) x b
⊢ (fun x => Real.exp (arg (f x) * (g x).im)) =Θ[l] fun x => 1
[PROOFSTEP]
refine' Real.isTheta_exp_comp_one.2 ⟨π * b, _⟩
[GOAL]
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => |(g x).im|) l, (fun x x_1 => x ≤ x_1) x b
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun x => |arg (f x) * (g x).im|) l, (fun x x_1 => x ≤ x_1) x (π * b)
[PROOFSTEP]
rw [eventually_map] at hb ⊢
[GOAL]
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) |(g a).im| b
⊢ ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) |arg (f a) * (g a).im| (π * b)
[PROOFSTEP]
refine' hb.mono fun x hx => _
[GOAL]
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) |(g a).im| b
x : α
hx : (fun x x_1 => x ≤ x_1) |(g x).im| b
⊢ (fun x x_1 => x ≤ x_1) |arg (f x) * (g x).im| (π * b)
[PROOFSTEP]
erw [abs_mul]
[GOAL]
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) |(g a).im| b
x : α
hx : (fun x x_1 => x ≤ x_1) |(g x).im| b
⊢ (fun x x_1 => x ≤ x_1) (|arg (f x)| * |(g x).im|) (π * b)
[PROOFSTEP]
exact mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) Real.pi_pos.le
[GOAL]
α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|
⊢ (let_fun this := fun x => ↑abs (f x) ^ (g x).re / 1;
    this) =ᶠ[l]
    let_fun this := fun x => ↑abs (f x) ^ (g x).re;
    this
[PROOFSTEP]
simp only [ofReal_one, div_one]
[GOAL]
α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|
⊢ (fun x => ↑abs (f x) ^ (g x).re) =ᶠ[l] fun x => ↑abs (f x) ^ (g x).re
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l : Filter α
f g : α → ℂ
hl_im : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|
hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0
⊢ (let_fun this := fun x => ↑abs (f x) ^ (g x).re / 1;
    this) =ᶠ[l]
    let_fun this := fun x => ↑abs (f x) ^ (g x).re;
    this
[PROOFSTEP]
simp only [ofReal_one, div_one]
[GOAL]
α : Type u_1
l : Filter α
f g : α → ℂ
hl_im : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|
hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0
⊢ (fun x => ↑abs (f x) ^ (g x).re) =ᶠ[l] fun x => ↑abs (f x) ^ (g x).re
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ ∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0
[PROOFSTEP]
convert hl
[GOAL]
case a
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0) ↔ b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
[PROOFSTEP]
rw [eventually_imp_distrib_right]
[GOAL]
case a
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ᶠ (x : α) in l, f x = 0) → b.re = 0 → b = 0 ↔ b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
[PROOFSTEP]
tauto
[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 (c ^ r) l (fun x => f x ^ r) fun x => g x ^ r
[PROOFSTEP]
apply IsBigOWith.of_bound
[GOAL]
case a
α : 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‖
[PROOFSTEP]
filter_upwards [hg, h.bound] with x hgx hx
[GOAL]
case h
α : 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 : OfNat.ofNat 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
[PROOFSTEP]
calc
  |f x ^ r| ≤ |f x| ^ r := abs_rpow_le_abs_rpow _ _
  _ ≤ (c * |g x|) ^ r := (rpow_le_rpow (abs_nonneg _) hx hr)
  _ = c ^ r * |g x ^ r| := by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]
[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 : OfNat.ofNat 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (c * |g x|) ^ r = c ^ r * |g x ^ r|
[PROOFSTEP]
rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]
[GOAL]
α : Type u_1
r c✝ : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ (c ^ r⁻¹) ^ r = c
[PROOFSTEP]
rw [← rpow_mul hc.le, inv_mul_cancel hr.ne', Real.rpow_one]
[GOAL]
s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => x ^ s / exp (b * x)) atTop (𝓝 0)
[PROOFSTEP]
simpa only [div_eq_mul_inv, exp_neg, neg_mul] using tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0 s b hb
[GOAL]
k : ℤ
b : ℝ
hb : 0 < b
⊢ (fun x => x ^ ↑k) =o[atTop] fun x => exp (b * x)
[PROOFSTEP]
simpa only [rpow_int_cast] using isLittleO_rpow_exp_pos_mul_atTop k hb
[GOAL]
k : ℕ
b : ℝ
hb : 0 < b
⊢ (fun x => x ^ ↑k) =o[atTop] fun x => exp (b * x)
[PROOFSTEP]
simpa using isLittleO_zpow_exp_pos_mul_atTop k hb
[GOAL]
s : ℝ
⊢ (fun x => x ^ s) =o[atTop] exp
[PROOFSTEP]
simpa only [one_mul] using isLittleO_rpow_exp_pos_mul_atTop s one_pos
[GOAL]
a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x => exp (-a * x)) =o[atTop] fun x => x ^ b
[PROOFSTEP]
apply isLittleO_of_tendsto'
[GOAL]
case hgf
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → exp (-a * x) = 0
[PROOFSTEP]
refine' (eventually_gt_atTop 0).mp (eventually_of_forall fun t ht h => _)
[GOAL]
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t ^ b = 0
⊢ exp (-a * t) = 0
[PROOFSTEP]
rw [rpow_eq_zero_iff_of_nonneg ht.le] at h 
[GOAL]
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t = 0 ∧ b ≠ 0
⊢ exp (-a * t) = 0
[PROOFSTEP]
exact (ht.ne' h.1).elim
[GOAL]
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x => exp (-a * x) / x ^ b) atTop (𝓝 0)
[PROOFSTEP]
refine' (tendsto_exp_mul_div_rpow_atTop (-b) a ha).inv_tendsto_atTop.congr' _
[GOAL]
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x => exp (a * x) / x ^ (-b))⁻¹ =ᶠ[atTop] fun x => exp (-a * x) / x ^ b
[PROOFSTEP]
refine' (eventually_ge_atTop 0).mp (eventually_of_forall fun t ht => _)
[GOAL]
case a
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 ≤ t
⊢ (fun x => exp (a * x) / x ^ (-b))⁻¹ t = (fun x => exp (-a * x) / x ^ b) t
[PROOFSTEP]
dsimp only
[GOAL]
case a
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 ≤ t
⊢ (fun x => exp (a * x) / x ^ (-b))⁻¹ t = exp (-a * t) / t ^ b
[PROOFSTEP]
rw [Pi.inv_apply, inv_div, ← inv_div_inv, neg_mul, Real.exp_neg, rpow_neg ht, inv_inv]
[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‖ ≤ 1 * ‖log x ^ r'‖
[PROOFSTEP]
have hx₀ : 0 ≤ log x := zero_le_one.trans hx
[GOAL]
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
hx₀ : 0 ≤ log x
⊢ ‖log x ^ r‖ ≤ 1 * ‖log x ^ r'‖
[PROOFSTEP]
simp [norm_eq_abs, abs_rpow_of_nonneg, abs_rpow_of_nonneg hx₀, rpow_le_rpow_of_exponent_le (hx.trans (le_abs_self _))]
[GOAL]
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
[PROOFSTEP]
simp only [← rpow_mul hx, div_mul_cancel _ hr.ne']
[GOAL]
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}
[PROOFSTEP]
simp [abs_of_nonpos, log_nonpos hx.1 hx.2]
[GOAL]
s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((fun x => x ^ (-s)) ∘ fun x => x⁻¹) x = (fun x => x ^ s) x
[PROOFSTEP]
rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv]
[GOAL]
r : ℝ
hr : r < 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x => (fun x => -|log x| ^ 1) x = log x) x}
[PROOFSTEP]
simp [abs_of_nonpos (log_nonpos hx.1 hx.2)]
[GOAL]
r : ℝ
hr : 0 < r
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ log x / x ^ (-r) = (fun x => log x * x ^ r) x
[PROOFSTEP]
rw [rpow_neg hx.out.le, div_inv_eq_mul]
