[GOAL]
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖exp (x + z) - exp x - z * exp x‖ = ‖exp x * (exp z - 1 - z)‖
[PROOFSTEP]
congr
[GOAL]
case e_a
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ exp (x + z) - exp x - z * exp x = exp x * (exp z - 1 - z)
[PROOFSTEP]
rw [exp_add]
[GOAL]
case e_a
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ exp x * exp z - exp x - z * exp x = exp x * (exp z - 1 - z)
[PROOFSTEP]
ring
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
have hy_eq : y = x + (y - x) := by abel
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ y = x + (y - x)
[PROOFSTEP]
abel
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ y = x + (y - x)
[PROOFSTEP]
abel
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
have hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖ := by
  rw [pow_two]
  exact mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
[PROOFSTEP]
rw [pow_two]
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ * ‖y - x‖ ≤ r * ‖y - x‖
[PROOFSTEP]
exact mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
have h_sq : ∀ z, ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2 :=
  by
  intro z hz
  have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
  rw [← sub_le_iff_le_add', ← norm_smul z]
  exact (norm_sub_norm_le _ _).trans this
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
[PROOFSTEP]
intro z hz
[GOAL]
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
[PROOFSTEP]
have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
[GOAL]
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
[PROOFSTEP]
rw [← sub_le_iff_le_add', ← norm_smul z]
[GOAL]
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp (x + z) - exp x‖ - ‖z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
[PROOFSTEP]
exact (norm_sub_norm_le _ _).trans this
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
calc
  ‖exp y - exp x‖ = ‖exp (x + (y - x)) - exp x‖ := by nth_rw 1 [hy_eq]
  _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * ‖y - x‖ ^ 2 := (h_sq (y - x) (hyx.le.trans hr_le))
  _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * (r * ‖y - x‖) :=
    (add_le_add_left (mul_le_mul le_rfl hyx_sq_le (sq_nonneg _) (norm_nonneg _)) _)
  _ = (1 + r) * ‖exp x‖ * ‖y - x‖ := by ring
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp y - exp x‖ = ‖exp (x + (y - x)) - exp x‖
[PROOFSTEP]
nth_rw 1 [hy_eq]
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * (r * ‖y - x‖) = (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
ring
[GOAL]
z y✝ x✝ : ℝ
x y : ℂ
⊢ dist y x < 1 → dist (exp y) (exp x) ≤ 2 * ‖exp x‖ * dist y x
[PROOFSTEP]
convert locally_lipschitz_exp zero_le_one le_rfl x y using 2
[GOAL]
case h'.h.e'_4
z y✝ x✝ : ℝ
x y : ℂ
a✝ : ‖y - x‖ < 1
⊢ 2 * ‖exp x‖ * dist y x = (1 + 1) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
congr
[GOAL]
case h'.h.e'_4.e_a.e_a
z y✝ x✝ : ℝ
x y : ℂ
a✝ : ‖y - x‖ < 1
⊢ 2 = 1 + 1
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
x✝ y z : ℝ
l : Filter α
x : ℝ
⊢ exp (x / 2) = sqrt (exp x)
[PROOFSTEP]
rw [eq_comm, sqrt_eq_iff_sq_eq, sq, ← exp_add, add_halves]
[GOAL]
case hx
α : Type u_1
x✝ y z : ℝ
l : Filter α
x : ℝ
⊢ 0 ≤ exp x
[PROOFSTEP]
exact (exp_pos _).le
[GOAL]
case hy
α : Type u_1
x✝ y z : ℝ
l : Filter α
x : ℝ
⊢ 0 ≤ exp (x / 2)
[PROOFSTEP]
exact (exp_pos _).le
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto exp atTop atTop
[PROOFSTEP]
have A : Tendsto (fun x : ℝ => x + 1) atTop atTop := tendsto_atTop_add_const_right atTop 1 tendsto_id
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
A : Tendsto (fun x => x + 1) atTop atTop
⊢ Tendsto exp atTop atTop
[PROOFSTEP]
have B : ∀ᶠ x in atTop, x + 1 ≤ exp x := eventually_atTop.2 ⟨0, fun x _ => add_one_le_exp x⟩
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
A : Tendsto (fun x => x + 1) atTop atTop
B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ exp x
⊢ Tendsto exp atTop atTop
[PROOFSTEP]
exact tendsto_atTop_mono' atTop B A
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto exp (𝓝 0) (𝓝 1)
[PROOFSTEP]
convert continuous_exp.tendsto 0
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
x y z : ℝ
l : Filter α
⊢ 1 = exp 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
⊢ Tendsto (fun x => exp x / x ^ n) atTop atTop
[PROOFSTEP]
refine' (atTop_basis_Ioi.tendsto_iff (atTop_basis' 1)).2 fun C hC₁ => _
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
[PROOFSTEP]
have hC₀ : 0 < C := zero_lt_one.trans_le hC₁
[GOAL]
α : Type u_1
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
[PROOFSTEP]
have : 0 < (exp 1 * C)⁻¹ := inv_pos.2 (mul_pos (exp_pos _) hC₀)
[GOAL]
α : Type u_1
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
[PROOFSTEP]
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))
[GOAL]
case intro
α : Type u_1
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
[PROOFSTEP]
simp only [← exp_nat_mul, mul_one, div_lt_iff, exp_pos, ← div_eq_inv_mul] at hN 
[GOAL]
case intro
α : Type u_1
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
[PROOFSTEP]
refine' ⟨N, trivial, fun x hx => _⟩
[GOAL]
case intro
α : Type u_1
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
[PROOFSTEP]
rw [Set.mem_Ioi] at hx 
[GOAL]
case intro
α : Type u_1
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
[PROOFSTEP]
have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx
[GOAL]
case intro
α : Type u_1
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
[PROOFSTEP]
rw [Set.mem_Ici, le_div_iff (pow_pos hx₀ _), ← le_div_iff' hC₀]
[GOAL]
case intro
α : Type u_1
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
[PROOFSTEP]
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']
[GOAL]
α : Type u_1
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)
[PROOFSTEP]
exact_mod_cast pow_le_pow_of_le_left hx₀.le (Nat.le_ceil _) _
[GOAL]
α : Type u_1
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)
[PROOFSTEP]
exact_mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
[GOAL]
α : Type u_1
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
[PROOFSTEP]
rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
[GOAL]
α : Type u_1
x✝ y z : ℝ
l : Filter α
n : ℕ
x : ℝ
⊢ ((fun r => r⁻¹) ∘ fun x => exp x / x ^ n) x = x ^ n * exp (-x)
[PROOFSTEP]
rw [comp_apply, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
⊢ Tendsto (fun x => (b * exp x + c) / x ^ n) atTop atTop
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => (b * exp x + c) / x ^ 0) atTop atTop
[PROOFSTEP]
simp only [pow_zero, div_one]
[GOAL]
case inl
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * exp x + c) atTop atTop
[PROOFSTEP]
exact (tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds
[GOAL]
case inr
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => (b * exp x + c) / x ^ n) atTop atTop
[PROOFSTEP]
simp only [add_div, mul_div_assoc]
[GOAL]
case inr
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => b * (exp x / x ^ n) + c / x ^ n) atTop atTop
[PROOFSTEP]
exact ((tendsto_exp_div_pow_atTop n).const_mul_atTop hb).atTop_add (tendsto_const_nhds.div_atTop (tendsto_pow_atTop hn))
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
[PROOFSTEP]
have H : ∀ d e, 0 < d → Tendsto (fun x : ℝ => x ^ n / (d * exp x + e)) atTop (𝓝 0) :=
  by
  intro b' c' h
  convert (tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1
  ext x
  simp
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
[PROOFSTEP]
intro b' c' h
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Tendsto (fun x => x ^ n / (b' * exp x + c')) atTop (𝓝 0)
[PROOFSTEP]
convert (tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1
[GOAL]
case h.e'_3
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ (fun x => x ^ n / (b' * exp x + c')) = (fun x => (b' * exp x + c') / x ^ n)⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
α : Type u_1
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
x : ℝ
⊢ x ^ n / (b' * exp x + c') = (fun x => (b' * exp x + c') / x ^ n)⁻¹ x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
[PROOFSTEP]
cases' lt_or_gt_of_ne hb with h h
[GOAL]
case inl
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 < b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
[PROOFSTEP]
exact H b c h
[GOAL]
case inr
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
[PROOFSTEP]
convert (H (-b) (-c) (neg_pos.mpr h)).neg using 1
[GOAL]
case h.e'_3
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ (fun x => x ^ n / (b * exp x + c)) = fun x => -(x ^ n / (-b * exp x + -c))
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
α : Type u_1
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * exp x + c) = -(x ^ n / (-b * exp x + -c))
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_3.h
α : Type u_1
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * exp x + c) = -x ^ n / (-(b * exp x) + -c)
[PROOFSTEP]
rw [← neg_add (b * exp x) c, neg_div_neg_eq]
[GOAL]
case h.e'_5
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ 𝓝 0 = 𝓝 (-0)
[PROOFSTEP]
rw [neg_zero]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x => { val := exp x, property := (_ : 0 < exp x) }) atTop atTop
[PROOFSTEP]
simp only [tendsto_Ioi_atTop, Subtype.coe_mk, tendsto_exp_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x => { val := exp x, property := (_ : 0 < exp x) }) atBot atBot
[PROOFSTEP]
simp [tendsto_exp_atBot_nhdsWithin]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Set.range exp = Set.Ioi 0
[PROOFSTEP]
rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Filter.map exp atTop = atTop
[PROOFSTEP]
rw [← coe_comp_expOrderIso, ← Filter.map_map, OrderIso.map_atTop, map_val_Ioi_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ comap exp atTop = atTop
[PROOFSTEP]
rw [← map_exp_atTop, comap_map exp_injective, map_exp_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x => exp (f x)) l atTop ↔ Tendsto f l atTop
[PROOFSTEP]
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (exp x)) atTop l ↔ Tendsto f atTop l
[PROOFSTEP]
simp_rw [← comp_apply (g := exp), ← tendsto_map'_iff, map_exp_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Filter.map exp atBot = 𝓝[Set.Ioi 0] 0
[PROOFSTEP]
rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ comap exp (𝓝[Set.Ioi 0] 0) = atBot
[PROOFSTEP]
rw [← map_exp_atBot, comap_map exp_injective]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (exp x)) atBot l ↔ Tendsto f (𝓝[Set.Ioi 0] 0) l
[PROOFSTEP]
rw [← map_exp_atBot, tendsto_map'_iff]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (exp x)) atBot l ↔ Tendsto (f ∘ exp) atBot l
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ comap exp (𝓝[Set.range exp] 0) = atBot
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x => exp (f x)) l (𝓝 0) ↔ Tendsto f l atBot
[PROOFSTEP]
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
⊢ (fun x => x ^ n) =o[atTop] exp
[PROOFSTEP]
simpa [isLittleO_iff_tendsto fun x hx => ((exp_pos x).ne' hx).elim] using
  tendsto_div_pow_mul_exp_add_atTop 1 0 n zero_ne_one
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f g : α → ℝ
⊢ (IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖exp (f x)‖ / ‖exp (g x)‖) ↔
    IsBoundedUnder (fun x x_1 => x ≤ x_1) l (f - g)
[PROOFSTEP]
simp only [norm_eq_abs, abs_exp, ← exp_sub, isBoundedUnder_le_exp_comp, Pi.sub_def]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f g : α → ℝ
⊢ ((fun x => exp (f x)) =Θ[l] fun x => exp (g x)) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |f x - g x|
[PROOFSTEP]
simp only [isBoundedUnder_le_abs, ← isBoundedUnder_le_neg, neg_sub, IsTheta, isBigO_exp_comp_exp_comp, Pi.sub_def]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f g : α → ℝ
⊢ ((fun x => exp (f x)) =o[l] fun x => exp (g x)) ↔ Tendsto (fun x => g x - f x) l atTop
[PROOFSTEP]
simp only [isLittleO_iff_tendsto, exp_ne_zero, ← exp_sub, ← tendsto_neg_atTop_iff, false_imp_iff, imp_true_iff,
  tendsto_exp_comp_nhds_zero, neg_sub]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => 1) =o[l] fun x => exp (f x)) ↔ Tendsto f l atTop
[PROOFSTEP]
simp only [← exp_zero, isLittleO_exp_comp_exp_comp, sub_zero]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => 1) =O[l] fun x => exp (f x)) ↔ IsBoundedUnder (fun x x_1 => x ≥ x_1) l f
[PROOFSTEP]
simp only [← exp_zero, isBigO_exp_comp_exp_comp, Pi.sub_def, zero_sub, isBoundedUnder_le_neg]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => exp (f x)) =O[l] fun x => 1) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
simp only [isBigO_one_iff, norm_eq_abs, abs_exp, isBoundedUnder_le_exp_comp]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => exp (f x)) =Θ[l] fun x => 1) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |f x|
[PROOFSTEP]
simp only [← exp_zero, isTheta_exp_comp_exp_comp, sub_zero]
[GOAL]
⊢ comap exp (comap (↑abs) atTop) = comap re (comap Real.exp atTop)
[PROOFSTEP]
simp only [comap_comap, (· ∘ ·), abs_exp]
[GOAL]
⊢ comap re (comap Real.exp atTop) = comap re atTop
[PROOFSTEP]
rw [Real.comap_exp_atTop]
[GOAL]
⊢ comap exp (𝓝 0) = comap re (comap Real.exp (𝓝 0))
[PROOFSTEP]
simp only [comap_comap, ← comap_abs_nhds_zero, (· ∘ ·), abs_exp]
[GOAL]
⊢ comap re (comap Real.exp (𝓝 0)) = comap re atBot
[PROOFSTEP]
rw [Real.comap_exp_nhds_zero]
[GOAL]
⊢ comap exp (𝓝[{0}ᶜ] 0) = comap re atBot
[PROOFSTEP]
have : (exp ⁻¹' {0})ᶜ = Set.univ := eq_univ_of_forall exp_ne_zero
[GOAL]
this : (exp ⁻¹' {0})ᶜ = Set.univ
⊢ comap exp (𝓝[{0}ᶜ] 0) = comap re atBot
[PROOFSTEP]
simp [nhdsWithin, comap_exp_nhds_zero, this]
[GOAL]
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x => exp (f x)) l (𝓝 0) ↔ Tendsto (fun x => (f x).re) l atBot
[PROOFSTEP]
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]
[GOAL]
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (re ∘ f) l atBot ↔ Tendsto (fun x => (f x).re) l atBot
[PROOFSTEP]
rfl
