α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
⊢ Tendsto (fun x => exp x / x ^ n) atTop atTop
refine' (atTop_basis_Ioi.tendsto_iff (atTop_basis' 1)).2 fun C hC₁ => _
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
have hC₀ : 0 < C := zero_lt_one.trans_le hC₁
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
have : 0 < (exp 1 * C)⁻¹ := inv_pos.2 (mul_pos (exp_pos _) hC₀)
case intro
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n / exp 1 ^ k < (exp 1 * C)⁻¹
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ k ≥ N, (↑k : ℝ) ^ n / exp 1 ^ k < (exp 1 * C)⁻¹ :=
  eventually_atTop.1
    ((tendsto_pow_const_div_const_pow_of_one_lt n (one_lt_exp_iff.2 zero_lt_one)).eventually
      (gt_mem_nhds this))
case intro
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
case intro
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n / exp 1 ^ k < (exp 1 * C)⁻¹
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
simp only [← exp_nat_mul, mul_one, div_lt_iff, exp_pos, ← div_eq_inv_mul] at hN
case intro
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : x ∈ Set.Ioi ↑N
⊢ exp x / x ^ n ∈ Set.Ici C
case intro
α : Type ?u.26645
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
refine' ⟨N, trivial, fun x hx => _⟩
case intro
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
⊢ exp x / x ^ n ∈ Set.Ici C
case intro
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : x ∈ Set.Ioi ↑N
⊢ exp x / x ^ n ∈ Set.Ici C
rw [Set.mem_Ioi] at hx
case intro
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ exp x / x ^ n ∈ Set.Ici C
case intro
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
⊢ exp x / x ^ n ∈ Set.Ici C
have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx
case intro
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ exp x / C
case intro
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ exp x / x ^ n ∈ Set.Ici C
rw [Set.mem_Ici, le_div_iff (pow_pos hx₀ _), ← le_div_iff' hC₀]
no goals
case intro
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ exp x / C
calc
  x ^ n ≤ ⌈x⌉₊ ^ n := by exact_mod_cast pow_le_pow_of_le_left hx₀.le (Nat.le_ceil _) _
  _ ≤ exp ⌈x⌉₊ / (exp 1 * C) := by exact_mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
  _ ≤ exp (x + 1) / (exp 1 * C) :=
    (div_le_div_of_le (mul_pos (exp_pos _) hC₀).le
      (exp_le_exp.2 <| (Nat.ceil_lt_add_one hx₀.le).le))
  _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
no goals
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ ↑(⌈x⌉₊ ^ n)
exact_mod_cast pow_le_pow_of_le_left hx₀.le (Nat.le_ceil _) _
no goals
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ ↑(⌈x⌉₊ ^ n) ≤ exp ↑⌈x⌉₊ / (exp 1 * C)
exact_mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
no goals
α : Type ?u.26645
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ exp (x + 1) / (exp 1 * C) = exp x / C
rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']