case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ Tendsto (fun x => exp x / x ^ s) atTop atTop
s : ℝ
⊢ Tendsto (fun x => exp x / x ^ s) atTop atTop
cases' archimedean_iff_nat_lt.1 Real.instArchimedean s with n hn
case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ (fun x => exp x / x ^ n) ≤ᶠ[atTop] fun x => exp x / x ^ s
case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ Tendsto (fun x => exp x / x ^ s) atTop atTop
refine' tendsto_atTop_mono' _ _ (tendsto_exp_div_pow_atTop n)
case h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ exp x / x ^ n ≤ exp x / x ^ s
case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ (fun x => exp x / x ^ n) ≤ᶠ[atTop] fun x => exp x / x ^ s
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_ge_atTop (1 : ℝ)]with x hx₀ hx₁
case h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ ↑n
case h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ exp x / x ^ n ≤ exp x / x ^ s
rw [div_le_div_left (exp_pos _) (pow_pos hx₀ _) (rpow_pos_of_pos hx₀ _), ← Real.rpow_nat_cast]
no goals
case h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ ↑n
exact rpow_le_rpow_of_exponent_le hx₁ hn.le