[GOAL]
x y : ℝ
hx : 0 < x
⊢ log x = ↑(OrderIso.symm expOrderIso) { val := x, property := hx }
[PROOFSTEP]
rw [log_of_ne_zero hx.ne']
[GOAL]
x y : ℝ
hx : 0 < x
⊢ ↑(OrderIso.symm expOrderIso) { val := |x|, property := (_ : 0 < |x|) } =
    ↑(OrderIso.symm expOrderIso) { val := x, property := hx }
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h.e_val
x y : ℝ
hx : 0 < x
⊢ |x| = x
[PROOFSTEP]
exact abs_of_pos hx
[GOAL]
x y : ℝ
hx : x ≠ 0
⊢ exp (log x) = |x|
[PROOFSTEP]
rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ exp (log x) = x
[PROOFSTEP]
rw [exp_log_eq_abs hx.ne']
[GOAL]
x y : ℝ
hx : 0 < x
⊢ |x| = x
[PROOFSTEP]
exact abs_of_pos hx
[GOAL]
x y : ℝ
hx : x < 0
⊢ exp (log x) = -x
[PROOFSTEP]
rw [exp_log_eq_abs (ne_of_lt hx)]
[GOAL]
x y : ℝ
hx : x < 0
⊢ |x| = -x
[PROOFSTEP]
exact abs_of_neg hx
[GOAL]
x✝ y x : ℝ
⊢ x ≤ exp (log x)
[PROOFSTEP]
by_cases h_zero : x = 0
[GOAL]
case pos
x✝ y x : ℝ
h_zero : x = 0
⊢ x ≤ exp (log x)
[PROOFSTEP]
rw [h_zero, log, dif_pos rfl, exp_zero]
[GOAL]
case pos
x✝ y x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
case neg
x✝ y x : ℝ
h_zero : ¬x = 0
⊢ x ≤ exp (log x)
[PROOFSTEP]
rw [exp_log_eq_abs h_zero]
[GOAL]
case neg
x✝ y x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|
[PROOFSTEP]
exact le_abs_self _
[GOAL]
x y : ℝ
⊢ exp (log 1) = exp 0
[PROOFSTEP]
rw [exp_log zero_lt_one, exp_zero]
[GOAL]
x✝ y x : ℝ
⊢ log |x| = log x
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
x✝ y x : ℝ
h : x = 0
⊢ log |x| = log x
[PROOFSTEP]
simp [h]
[GOAL]
case neg
x✝ y x : ℝ
h : ¬x = 0
⊢ log |x| = log x
[PROOFSTEP]
rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]
[GOAL]
x✝ y x : ℝ
⊢ log (-x) = log x
[PROOFSTEP]
rw [← log_abs x, ← log_abs (-x), abs_neg]
[GOAL]
x✝ y x : ℝ
hx : 0 < x
⊢ sinh (log x) = (x - x⁻¹) / 2
[PROOFSTEP]
rw [sinh_eq, exp_neg, exp_log hx]
[GOAL]
x✝ y x : ℝ
hx : 0 < x
⊢ cosh (log x) = (x + x⁻¹) / 2
[PROOFSTEP]
rw [cosh_eq, exp_neg, exp_log hx]
[GOAL]
x✝¹ y x : ℝ
x✝ : x ∈ univ
⊢ log (-exp x) = x
[PROOFSTEP]
rw [log_neg_eq_log, log_exp]
[GOAL]
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ exp (log (x * y)) = exp (log x + log y)
[PROOFSTEP]
rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]
[GOAL]
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ exp (log (x / y)) = exp (log x - log y)
[PROOFSTEP]
rw [exp_log_eq_abs (div_ne_zero hx hy), exp_sub, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_div]
[GOAL]
x✝ y x : ℝ
⊢ log x⁻¹ = -log x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
x✝ y x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
x✝ y x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x
[PROOFSTEP]
rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
[GOAL]
x y : ℝ
h : 0 < x
h₁ : 0 < y
⊢ log x ≤ log y ↔ x ≤ y
[PROOFSTEP]
rw [← exp_le_exp, exp_log h, exp_log h₁]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ x < y → log x < log y
[PROOFSTEP]
intro h
[GOAL]
x y : ℝ
hx : 0 < x
h : x < y
⊢ log x < log y
[PROOFSTEP]
rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ x ≤ y → log x ≤ log y
[PROOFSTEP]
intro hxy
[GOAL]
x y : ℝ
hx : 0 < x
hxy : x ≤ y
⊢ log x ≤ log y
[PROOFSTEP]
cases hxy.eq_or_lt with
| inl h_eq => simp [h_eq]
| inr hlt => exact le_of_lt <| log_lt_log hx hlt
[GOAL]
x y : ℝ
hx : 0 < x
hxy : x ≤ y
x✝ : x = y ∨ x < y
⊢ log x ≤ log y
[PROOFSTEP]
cases hxy.eq_or_lt with
| inl h_eq => simp [h_eq]
| inr hlt => exact le_of_lt <| log_lt_log hx hlt
[GOAL]
case inl
x y : ℝ
hx : 0 < x
hxy : x ≤ y
h_eq : x = y
⊢ log x ≤ log y
[PROOFSTEP]

| inl h_eq => simp [h_eq]
[GOAL]
case inl
x y : ℝ
hx : 0 < x
hxy : x ≤ y
h_eq : x = y
⊢ log x ≤ log y
[PROOFSTEP]
simp [h_eq]
[GOAL]
case inr
x y : ℝ
hx : 0 < x
hxy : x ≤ y
hlt : x < y
⊢ log x ≤ log y
[PROOFSTEP]

| inr hlt => exact le_of_lt <| log_lt_log hx hlt
[GOAL]
case inr
x y : ℝ
hx : 0 < x
hxy : x ≤ y
hlt : x < y
⊢ log x ≤ log y
[PROOFSTEP]
exact le_of_lt <| log_lt_log hx hlt
[GOAL]
x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y
[PROOFSTEP]
rw [← exp_lt_exp, exp_log hx, exp_log hy]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ log x ≤ y ↔ x ≤ exp y
[PROOFSTEP]
rw [← exp_le_exp, exp_log hx]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ log x < y ↔ x < exp y
[PROOFSTEP]
rw [← exp_lt_exp, exp_log hx]
[GOAL]
x y : ℝ
hy : 0 < y
⊢ x ≤ log y ↔ exp x ≤ y
[PROOFSTEP]
rw [← exp_le_exp, exp_log hy]
[GOAL]
x y : ℝ
hy : 0 < y
⊢ x < log y ↔ exp x < y
[PROOFSTEP]
rw [← exp_lt_exp, exp_log hy]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ 0 < log x ↔ 1 < x
[PROOFSTEP]
rw [← log_one]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ log 1 < log x ↔ 1 < x
[PROOFSTEP]
exact log_lt_log_iff zero_lt_one hx
[GOAL]
x y : ℝ
hx : x < -1
⊢ 0 < log x
[PROOFSTEP]
rw [← neg_neg x, log_neg_eq_log]
[GOAL]
x y : ℝ
hx : x < -1
⊢ 0 < log (-x)
[PROOFSTEP]
have : 1 < -x := by linarith
[GOAL]
x y : ℝ
hx : x < -1
⊢ 1 < -x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx : x < -1
this : 1 < -x
⊢ 0 < log (-x)
[PROOFSTEP]
exact log_pos this
[GOAL]
x y : ℝ
h : 0 < x
⊢ log x < 0 ↔ x < 1
[PROOFSTEP]
rw [← log_one]
[GOAL]
x y : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1
[PROOFSTEP]
exact log_lt_log_iff h zero_lt_one
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log x < 0
[PROOFSTEP]
rw [← neg_neg x, log_neg_eq_log]
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log (-x) < 0
[PROOFSTEP]
have h0' : 0 < -x := by linarith
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
⊢ 0 < -x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ log (-x) < 0
[PROOFSTEP]
have h1' : -x < 1 := by linarith
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ -x < 1
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
h1' : -x < 1
⊢ log (-x) < 0
[PROOFSTEP]
exact log_neg h0' h1'
[GOAL]
x y : ℝ
hx : 0 < x
⊢ 0 ≤ log x ↔ 1 ≤ x
[PROOFSTEP]
rw [← not_lt, log_neg_iff hx, not_lt]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1
[PROOFSTEP]
rw [← not_lt, log_pos_iff hx, not_lt]
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ log x ≤ 0 ↔ x ≤ 1
[PROOFSTEP]
rcases hx.eq_or_lt with (rfl | hx)
[GOAL]
case inl
y : ℝ
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1
[PROOFSTEP]
simp [le_refl, zero_le_one]
[GOAL]
case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1
[PROOFSTEP]
exact log_nonpos_iff hx
[GOAL]
x y : ℝ
n : ℕ
⊢ 0 ≤ log ↑n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
x y : ℝ
n : ℕ
hn : n = 0
⊢ 0 ≤ log ↑n
case neg x y : ℝ n : ℕ hn : ¬n = 0 ⊢ 0 ≤ log ↑n
[PROOFSTEP]
case pos => simp [hn]
[GOAL]
x y : ℝ
n : ℕ
hn : n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
case pos => simp [hn]
[GOAL]
x y : ℝ
n : ℕ
hn : n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
x y : ℝ
n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
case neg =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
  exact log_nonneg this
[GOAL]
x y : ℝ
n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
case neg =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
  exact log_nonneg this
[GOAL]
x y : ℝ
n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
have : (1 : ℝ) ≤ n := by exact_mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
[GOAL]
x y : ℝ
n : ℕ
hn : ¬n = 0
⊢ 1 ≤ ↑n
[PROOFSTEP]
exact_mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
[GOAL]
x y : ℝ
n : ℕ
hn : ¬n = 0
this : 1 ≤ ↑n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
exact log_nonneg this
[GOAL]
x y : ℝ
n : ℕ
⊢ 0 ≤ log (-↑n)
[PROOFSTEP]
rw [← log_neg_eq_log, neg_neg]
[GOAL]
x y : ℝ
n : ℕ
⊢ 0 ≤ log ↑n
[PROOFSTEP]
exact log_nat_cast_nonneg _
[GOAL]
x y : ℝ
n : ℤ
⊢ 0 ≤ log ↑n
[PROOFSTEP]
cases lt_trichotomy 0 n with
| inl hn =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast hn
  exact log_nonneg this
| inr hn =>
  cases hn with
  | inl hn => simp [hn.symm]
  | inr hn =>
    have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
    rw [← log_neg_eq_log]
    exact log_nonneg this
[GOAL]
x y : ℝ
n : ℤ
x✝ : 0 < n ∨ 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
cases lt_trichotomy 0 n with
| inl hn =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast hn
  exact log_nonneg this
| inr hn =>
  cases hn with
  | inl hn => simp [hn.symm]
  | inr hn =>
    have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
    rw [← log_neg_eq_log]
    exact log_nonneg this
[GOAL]
case inl
x y : ℝ
n : ℤ
hn : 0 < n
⊢ 0 ≤ log ↑n
[PROOFSTEP]

| inl hn =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast hn
  exact log_nonneg this
[GOAL]
case inl
x y : ℝ
n : ℤ
hn : 0 < n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
have : (1 : ℝ) ≤ n := by exact_mod_cast hn
[GOAL]
x y : ℝ
n : ℤ
hn : 0 < n
⊢ 1 ≤ ↑n
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case inl
x y : ℝ
n : ℤ
hn : 0 < n
this : 1 ≤ ↑n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
exact log_nonneg this
[GOAL]
case inr
x y : ℝ
n : ℤ
hn : 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]

| inr hn =>
  cases hn with
  | inl hn => simp [hn.symm]
  | inr hn =>
    have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
    rw [← log_neg_eq_log]
    exact log_nonneg this
[GOAL]
case inr
x y : ℝ
n : ℤ
hn : 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
cases hn with
| inl hn => simp [hn.symm]
| inr hn =>
  have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
  rw [← log_neg_eq_log]
  exact log_nonneg this
[GOAL]
case inr
x y : ℝ
n : ℤ
hn : 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
cases hn with
| inl hn => simp [hn.symm]
| inr hn =>
  have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
  rw [← log_neg_eq_log]
  exact log_nonneg this
[GOAL]
case inr.inl
x y : ℝ
n : ℤ
hn : 0 = n
⊢ 0 ≤ log ↑n
[PROOFSTEP]

| inl hn => simp [hn.symm]
[GOAL]
case inr.inl
x y : ℝ
n : ℤ
hn : 0 = n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
simp [hn.symm]
[GOAL]
case inr.inr
x y : ℝ
n : ℤ
hn : n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]

| inr hn =>
  have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
  rw [← log_neg_eq_log]
  exact log_nonneg this
[GOAL]
case inr.inr
x y : ℝ
n : ℤ
hn : n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
[GOAL]
x y : ℝ
n : ℤ
hn : n < 0
⊢ 1 ≤ -↑n
[PROOFSTEP]
rw [← neg_zero, ← lt_neg] at hn
[GOAL]
x y : ℝ
n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case inr.inr
x y : ℝ
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
rw [← log_neg_eq_log]
[GOAL]
case inr.inr
x y : ℝ
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log (-↑n)
[PROOFSTEP]
exact log_nonneg this
[GOAL]
x y : ℝ
⊢ StrictAntiOn log (Iio 0)
[PROOFSTEP]
rintro x (hx : x < 0) y (hy : y < 0) hxy
[GOAL]
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log y < log x
[PROOFSTEP]
rw [← log_abs y, ← log_abs x]
[GOAL]
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log |y| < log |x|
[PROOFSTEP]
refine' log_lt_log (abs_pos.2 hy.ne) _
[GOAL]
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|
[PROOFSTEP]
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]
[GOAL]
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x < x - 1
[PROOFSTEP]
have h : log x ≠ 0
[GOAL]
case h
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x ≠ 0
[PROOFSTEP]
rwa [← log_one, log_injOn_pos.ne_iff hx1]
[GOAL]
case h
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ 1 ∈ Ioi 0
[PROOFSTEP]
exact mem_Ioi.mpr zero_lt_one
[GOAL]
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
h : log x ≠ 0
⊢ log x < x - 1
[PROOFSTEP]
linarith [add_one_lt_exp_of_nonzero h, exp_log hx1]
[GOAL]
x✝ y x : ℝ
⊢ log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
constructor
[GOAL]
case mp
x✝ y x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
intro h
[GOAL]
case mp
x✝ y x : ℝ
h : log x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)
[GOAL]
case mp.inl
x✝ y x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
refine' Or.inr (Or.inr (neg_eq_iff_eq_neg.mp _))
[GOAL]
case mp.inl
x✝ y x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1
[PROOFSTEP]
rw [← log_neg_eq_log x] at h
[GOAL]
case mp.inl
x✝ y x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1
[PROOFSTEP]
exact eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h
[GOAL]
case mp.inr.inl
x y : ℝ
h : log 0 = 0
⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = -1
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case mp.inr.inr
x✝ y x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
exact Or.inr (Or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h))
[GOAL]
case mpr
x✝ y x : ℝ
⊢ x = 0 ∨ x = 1 ∨ x = -1 → log x = 0
[PROOFSTEP]
rintro (rfl | rfl | rfl)
[GOAL]
case mpr.inl
x y : ℝ
⊢ log 0 = 0
[PROOFSTEP]
simp only [log_one, log_zero, log_neg_eq_log]
[GOAL]
case mpr.inr.inl
x y : ℝ
⊢ log 1 = 0
[PROOFSTEP]
simp only [log_one, log_zero, log_neg_eq_log]
[GOAL]
case mpr.inr.inr
x y : ℝ
⊢ log (-1) = 0
[PROOFSTEP]
simp only [log_one, log_zero, log_neg_eq_log]
[GOAL]
x✝ y x : ℝ
⊢ log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1
[PROOFSTEP]
simpa only [not_or] using log_eq_zero.not
[GOAL]
x✝ y x : ℝ
n : ℕ
⊢ log (x ^ n) = ↑n * log x
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
x✝ y x : ℝ
⊢ log (x ^ Nat.zero) = ↑Nat.zero * log x
[PROOFSTEP]
simp
[GOAL]
case succ
x✝ y x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
⊢ log (x ^ Nat.succ n) = ↑(Nat.succ n) * log x
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case succ.inl
x y : ℝ
n : ℕ
ih : log (0 ^ n) = ↑n * log 0
⊢ log (0 ^ Nat.succ n) = ↑(Nat.succ n) * log 0
[PROOFSTEP]
simp
[GOAL]
case succ.inr
x✝ y x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ Nat.succ n) = ↑(Nat.succ n) * log x
[PROOFSTEP]
rw [pow_succ', log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
[GOAL]
x✝ y x : ℝ
n : ℤ
⊢ log (x ^ n) = ↑n * log x
[PROOFSTEP]
induction n
[GOAL]
case ofNat
x✝ y x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.ofNat a✝) = ↑(Int.ofNat a✝) * log x
[PROOFSTEP]
rw [Int.ofNat_eq_coe, zpow_ofNat, log_pow, Int.cast_ofNat]
[GOAL]
case negSucc
x✝ y x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.negSucc a✝) = ↑(Int.negSucc a✝) * log x
[PROOFSTEP]
rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]
[GOAL]
x✝ y x : ℝ
hx : 0 ≤ x
⊢ log (sqrt x) = log x / 2
[PROOFSTEP]
rw [eq_div_iff, mul_comm, ← Nat.cast_two, ← log_pow, sq_sqrt hx]
[GOAL]
x✝ y x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0
[PROOFSTEP]
exact two_ne_zero
[GOAL]
x✝ y x : ℝ
hx : 0 < x
⊢ log x ≤ x - 1
[PROOFSTEP]
rw [le_sub_iff_add_le]
[GOAL]
x✝ y x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x
[PROOFSTEP]
convert add_one_le_exp (log x)
[GOAL]
case h.e'_4
x✝ y x : ℝ
hx : 0 < x
⊢ x = exp (log x)
[PROOFSTEP]
rw [exp_log hx]
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ |log x * x| < 1
[PROOFSTEP]
have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ 0 < 1 / x
[PROOFSTEP]
simpa only [one_div, inv_pos] using h1
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 < 1 / x
⊢ |log x * x| < 1
[PROOFSTEP]
replace := log_le_sub_one_of_pos this
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ |log x * x| < 1
[PROOFSTEP]
replace : log (1 / x) < 1 / x := by linarith
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ log (1 / x) < 1 / x
[PROOFSTEP]
linarith
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) < 1 / x
⊢ |log x * x| < 1
[PROOFSTEP]
rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff h1] at this
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ |log x * x| < 1
[PROOFSTEP]
have aux : 0 ≤ -log x * x := by
  refine' mul_nonneg _ h1.le
  rw [← log_inv]
  apply log_nonneg
  rw [← le_inv h1 zero_lt_one, inv_one]
  exact h2
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x * x
[PROOFSTEP]
refine' mul_nonneg _ h1.le
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x
[PROOFSTEP]
rw [← log_inv]
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹
[PROOFSTEP]
apply log_nonneg
[GOAL]
case hx
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 1 ≤ x⁻¹
[PROOFSTEP]
rw [← le_inv h1 zero_lt_one, inv_one]
[GOAL]
case hx
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1
[PROOFSTEP]
exact h2
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1
[PROOFSTEP]
rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : |log x * x| < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1
[PROOFSTEP]
exact this
[GOAL]
x y : ℝ
⊢ Tendsto (fun x => log (exp x)) atTop atTop
[PROOFSTEP]
simpa only [log_exp] using tendsto_id
[GOAL]
x y : ℝ
⊢ Tendsto log (𝓝[{0}ᶜ] 0) atBot
[PROOFSTEP]
rw [← show _ = log from funext log_abs]
[GOAL]
x y : ℝ
⊢ Tendsto (fun x => log |x|) (𝓝[{0}ᶜ] 0) atBot
[PROOFSTEP]
refine' Tendsto.comp (g := log) _ tendsto_abs_nhdsWithin_zero
[GOAL]
x y : ℝ
⊢ Tendsto log (𝓝[Ioi 0] 0) atBot
[PROOFSTEP]
simpa [← tendsto_comp_exp_atBot] using tendsto_id
[GOAL]
x y : ℝ
⊢ ContinuousOn log {0}ᶜ
[PROOFSTEP]
simp only [continuousOn_iff_continuous_restrict, restrict]
[GOAL]
x y : ℝ
⊢ Continuous fun x => log ↑x
[PROOFSTEP]
conv in log _ => rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
[GOAL]
x✝ y : ℝ
x : ↑{0}ᶜ
| log ↑x
[PROOFSTEP]
rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
[GOAL]
x✝ y : ℝ
x : ↑{0}ᶜ
| log ↑x
[PROOFSTEP]
rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
[GOAL]
x✝ y : ℝ
x : ↑{0}ᶜ
| log ↑x
[PROOFSTEP]
rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
[GOAL]
x y : ℝ
⊢ Continuous fun x => ↑(OrderIso.symm expOrderIso) { val := |↑x|, property := (_ : 0 < |↑x|) }
[PROOFSTEP]
exact expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)
[GOAL]
x y : ℝ
⊢ ContinuousAt log x ↔ x ≠ 0
[PROOFSTEP]
refine' ⟨_, continuousAt_log⟩
[GOAL]
x y : ℝ
⊢ ContinuousAt log x → x ≠ 0
[PROOFSTEP]
rintro h rfl
[GOAL]
y : ℝ
h : ContinuousAt log 0
⊢ False
[PROOFSTEP]
exact not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsWithin_zero _ (h.tendsto.mono_left inf_le_left)
[GOAL]
x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (x : α), x ∈ s → f x ≠ 0
⊢ log (∏ i in s, f i) = ∑ i in s, log (f i)
[PROOFSTEP]
induction' s using Finset.cons_induction_on with a s ha ih
[GOAL]
case h₁
x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s → f x ≠ 0
hf : ∀ (x : α), x ∈ ∅ → f x ≠ 0
⊢ log (∏ i in ∅, f i) = ∑ i in ∅, log (f i)
[PROOFSTEP]
simp
[GOAL]
case h₂
x y : ℝ
α : Type u_1
s✝ : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s✝ → f x ≠ 0
a : α
s : Finset α
ha : ¬a ∈ s
ih : (∀ (x : α), x ∈ s → f x ≠ 0) → log (∏ i in s, f i) = ∑ i in s, log (f i)
hf : ∀ (x : α), x ∈ Finset.cons a s ha → f x ≠ 0
⊢ log (∏ i in Finset.cons a s ha, f i) = ∑ i in Finset.cons a s ha, log (f i)
[PROOFSTEP]
rw [Finset.forall_mem_cons] at hf
[GOAL]
case h₂
x y : ℝ
α : Type u_1
s✝ : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s✝ → f x ≠ 0
a : α
s : Finset α
ha : ¬a ∈ s
ih : (∀ (x : α), x ∈ s → f x ≠ 0) → log (∏ i in s, f i) = ∑ i in s, log (f i)
hf : f a ≠ 0 ∧ ∀ (x : α), x ∈ s → f x ≠ 0
⊢ log (∏ i in Finset.cons a s ha, f i) = ∑ i in Finset.cons a s ha, log (f i)
[PROOFSTEP]
simp [ih hf.2, log_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)]
[GOAL]
x y : ℝ
n : ℕ
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => ↑t * log ↑p
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
x y : ℝ
⊢ log ↑0 = Finsupp.sum (Nat.factorization 0) fun p t => ↑t * log ↑p
[PROOFSTEP]
simp
  -- relies on junk values of `log` and `Nat.factorization`
[GOAL]
case inr
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => ↑t * log ↑p
[PROOFSTEP]
simp only [← log_pow, ← Nat.cast_pow]
[GOAL]
case inr
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => log ↑(p ^ t)
[PROOFSTEP]
rw [← Finsupp.log_prod, ← Nat.cast_finsupp_prod, Nat.factorization_prod_pow_eq_self hn]
[GOAL]
case inr.hg
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ ↑(Nat.factorization n) a) = 0 → ↑(Nat.factorization n) a = 0
[PROOFSTEP]
intro p hp
[GOAL]
case inr.hg
x y : ℝ
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ ↑(Nat.factorization n) p) = 0
⊢ ↑(Nat.factorization n) p = 0
[PROOFSTEP]
rw [pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]
[GOAL]
x y a b : ℝ
n : ℕ
ha : a ≠ 0
⊢ (fun x => x ^ n / (a * exp x + b)) ∘ log =ᶠ[atTop] fun x => log x ^ n / (a * x + b)
[PROOFSTEP]
filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]
[GOAL]
x✝ y a b : ℝ
n : ℕ
ha : a ≠ 0
x : ℝ
hx : 0 < x
⊢ ((fun x => x ^ n / (a * exp x + b)) ∘ log) x = log x ^ n / (a * x + b)
[PROOFSTEP]
simp [exp_log hx]
[GOAL]
x y : ℝ
n : ℕ
⊢ (fun x => log x ^ n) =o[atTop] id
[PROOFSTEP]
rw [Asymptotics.isLittleO_iff_tendsto']
[GOAL]
x y : ℝ
n : ℕ
⊢ Tendsto (fun x => log x ^ n / id x) atTop (𝓝 0)
[PROOFSTEP]
simpa using tendsto_pow_log_div_mul_add_atTop 1 0 n one_ne_zero
[GOAL]
x y : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
[PROOFSTEP]
filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim
[GOAL]
x y c : ℝ
⊢ (fun x => c) =o[atTop] log
[PROOFSTEP]
refine Asymptotics.isLittleO_of_tendsto' ?_ <| Tendsto.div_atTop (a := c) (by simp) tendsto_log_atTop
[GOAL]
x y c : ℝ
⊢ Tendsto (fun x => c) atTop (𝓝 c)
[PROOFSTEP]
simp
[GOAL]
x y c : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, log x = 0 → c = 0
[PROOFSTEP]
filter_upwards [eventually_gt_atTop 1] with x hx
[GOAL]
case h
x✝ y c x : ℝ
hx : 1 < x
⊢ log x = 0 → c = 0
[PROOFSTEP]
aesop (add safe forward log_pos)
[GOAL]
y : ℝ
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
[PROOFSTEP]
have : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
[GOAL]
case this
y : ℝ
⊢ Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
[PROOFSTEP]
exact tendsto_const_nhds.add (tendsto_const_nhds.div_atTop tendsto_id)
[GOAL]
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
[PROOFSTEP]
rw [← comap_exp_nhds_exp, exp_zero, tendsto_comap_iff, ← add_zero (1 : ℝ)]
[GOAL]
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (exp ∘ fun x => log (x + y) - log x) atTop (𝓝 (1 + 0))
[PROOFSTEP]
refine' this.congr' _
[GOAL]
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ (fun x => 1 + y / x) =ᶠ[atTop] exp ∘ fun x => log (x + y) - log x
[PROOFSTEP]
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_gt_atTop (-y)] with x hx₀ hxy
[GOAL]
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (exp ∘ fun x => log (x + y) - log x) x
[PROOFSTEP]
rw [comp_apply, exp_sub, exp_log, exp_log, one_add_div]
[GOAL]
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ x ≠ 0
[PROOFSTEP]
linarith
[GOAL]
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x
[PROOFSTEP]
linarith
[GOAL]
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y
[PROOFSTEP]
linarith
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log e
[PROOFSTEP]
rw [NormNum.IsNat.to_eq h rfl]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log ↑n
[PROOFSTEP]
exact Real.log_nat_cast_nonneg _
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log e
[PROOFSTEP]
rw [NormNum.IsNat.to_eq h rfl]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n
[PROOFSTEP]
apply Real.log_pos
[GOAL]
case hx
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 1 < ↑n
[PROOFSTEP]
simpa using w
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log e
[PROOFSTEP]
rw [NormNum.IsInt.neg_to_eq h rfl]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-↑n)
[PROOFSTEP]
exact Real.log_neg_nat_cast_nonneg _
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log e
[PROOFSTEP]
rw [NormNum.IsInt.neg_to_eq h rfl]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log (-↑n)
[PROOFSTEP]
rw [Real.log_neg_eq_log]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n
[PROOFSTEP]
apply Real.log_pos
[GOAL]
case hx
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 1 < ↑n
[PROOFSTEP]
simpa using w
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log e
[PROOFSTEP]
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log (↑n / ↑d)
[PROOFSTEP]
have : 1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 1 < ↑n / ↑d
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
this : 1 < ↑n / ↑d
⊢ 0 < Real.log (↑n / ↑d)
[PROOFSTEP]
exact Real.log_pos this
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log e
[PROOFSTEP]
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log (↑n / ↑d)
[PROOFSTEP]
have : (n : ℝ) / d < -1 := by exact_mod_cast of_decide_eq_true h
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ ↑n / ↑d < -1
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
this : ↑n / ↑d < -1
⊢ 0 < Real.log (↑n / ↑d)
[PROOFSTEP]
exact Real.log_pos_of_lt_neg_one this
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log e ≠ 0
[PROOFSTEP]
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
have h₁' : 0 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₁
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ 0 < ↑n / ↑d
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h₁
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
have h₂' : (n : ℝ) / d < 1 := by exact_mod_cast of_decide_eq_true h₂
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ ↑n / ↑d < 1
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h₂
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
h₂' : ↑n / ↑d < 1
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
exact ne_of_lt <| Real.log_neg h₁' h₂'
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ Real.log e ≠ 0
[PROOFSTEP]
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
have h₁' : (n : ℝ) / d < 0 := by exact_mod_cast of_decide_eq_true h₁
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ ↑n / ↑d < 0
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h₁
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
have h₂' : -1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₂
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
⊢ -1 < ↑n / ↑d
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h₂
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
h₂' : -1 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
exact ne_of_lt <| Real.log_neg_of_lt_zero h₁' h₂'
[GOAL]
$x✝ : Type x✝
«$_zα» : Zero $x✝
«$_pα» : PartialOrder $x✝
«$e» : $x✝
«$f» : ℝ → ℝ
«$a» : ℝ
«$n» : ℤ
«$d» : ℕ
«$i» : DivisionRing ℝ := Real.instDivisionRingReal
«$p» : NormNum.IsRat «$a» «$n» «$d»
⊢ Sort ?u.471336
[PROOFSTEP]
clear! «$i»
[GOAL]
$x✝ : Type x✝
«$_zα» : Zero $x✝
«$_pα» : PartialOrder $x✝
«$e» : $x✝
«$f» : ℝ → ℝ
«$a» : ℝ
«$n» : ℤ
«$d» : ℕ
⊢ Sort ?u.471336
[PROOFSTEP]
exact NormNum.IsRat «$a» «$n» «$d»


[GOAL]
x : ℂ
⊢ x ^ 0 = 1
[PROOFSTEP]
simp [cpow_def]
[GOAL]
x y : ℂ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp only [cpow_def]
[GOAL]
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp [*, exp_ne_zero]
[GOAL]
case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp [*, exp_ne_zero]
[GOAL]
case neg
x y : ℂ
h✝ : ¬x = 0
⊢ exp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp [*, exp_ne_zero]
[GOAL]
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0
[PROOFSTEP]
simp [cpow_def, *]
[GOAL]
x a : ℂ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
x a : ℂ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
intro hyp
[GOAL]
case mp
x a : ℂ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
simp only [cpow_def, eq_self_iff_true, if_true] at hyp
[GOAL]
case mp
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
by_cases x = 0
[GOAL]
case mp
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
by_cases x = 0
[GOAL]
case pos
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
subst h
[GOAL]
case pos
a : ℂ
hyp : (if 0 = 0 then 1 else 0) = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
[PROOFSTEP]
simp only [if_true, eq_self_iff_true] at hyp
[GOAL]
case pos
a : ℂ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
[PROOFSTEP]
right
[GOAL]
case pos.h
a : ℂ
hyp : 1 = a
⊢ 0 = 0 ∧ a = 1
[PROOFSTEP]
exact ⟨rfl, hyp.symm⟩
[GOAL]
case neg
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
rw [if_neg h] at hyp
[GOAL]
case neg
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
left
[GOAL]
case neg.h
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0
[PROOFSTEP]
exact ⟨h, hyp.symm⟩
[GOAL]
case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a
[PROOFSTEP]
rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case mpr.inl.intro
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0
[PROOFSTEP]
exact zero_cpow h
[GOAL]
case mpr.inr.intro
⊢ 0 ^ 0 = 1
[PROOFSTEP]
exact cpow_zero _
[GOAL]
x a : ℂ
⊢ a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
rw [← zero_cpow_eq_iff, eq_comm]
[GOAL]
x : ℂ
hx : x = 0
⊢ x ^ 1 = x
[PROOFSTEP]
simp [hx, cpow_def]
[GOAL]
x : ℂ
hx : ¬x = 0
⊢ x ^ 1 = x
[PROOFSTEP]
rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]
[GOAL]
x : ℂ
⊢ 1 ^ x = 1
[PROOFSTEP]
rw [cpow_def]
[GOAL]
x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else exp (log 1 * x)) = 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x : ℂ
h✝¹ : 1 = 0
h✝ : x = 0
⊢ 1 = 1
[PROOFSTEP]
simp_all [one_ne_zero]
[GOAL]
case neg
x : ℂ
h✝¹ : 1 = 0
h✝ : ¬x = 0
⊢ 0 = 1
[PROOFSTEP]
simp_all [one_ne_zero]
[GOAL]
case neg
x : ℂ
h✝ : ¬1 = 0
⊢ exp (log 1 * x) = 1
[PROOFSTEP]
simp_all [one_ne_zero]
[GOAL]
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z
[PROOFSTEP]
simp only [cpow_def, ite_mul, boole_mul, mul_ite, mul_boole]
[GOAL]
x y z : ℂ
hx : x ≠ 0
⊢ (if x = 0 then if y + z = 0 then 1 else 0 else exp (log x * (y + z))) =
    if x = 0 then
      if z = 0 then if x = 0 then if y = 0 then 1 * 1 else 0 * 1 else exp (log x * y) * 1
      else if x = 0 then if y = 0 then 1 * 0 else 0 * 0 else exp (log x * y) * 0
    else if x = 0 then if y = 0 then 1 * exp (log x * z) else 0 * exp (log x * z) else exp (log x * y) * exp (log x * z)
[PROOFSTEP]
simp_all [exp_add, mul_add]
[GOAL]
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ x ^ (y * z) = (x ^ y) ^ z
[PROOFSTEP]
simp only [cpow_def]
[GOAL]
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else exp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) = 0 then if z = 0 then 1 else 0
    else exp (log (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) * z)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : z = 0
⊢ 1 = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : ¬z = 0
⊢ 1 = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : y * z = 0
h✝¹ : y = 0
h✝ : ¬1 = 0
⊢ 1 = exp (log 1 * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : z = 0
⊢ 1 = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : ¬z = 0
⊢ 1 = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : y * z = 0
h✝¹ : ¬y = 0
h✝ : ¬0 = 0
⊢ 1 = exp (log 0 * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : z = 0
⊢ 0 = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : ¬z = 0
⊢ 0 = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : ¬y * z = 0
h✝¹ : y = 0
h✝ : ¬1 = 0
⊢ 0 = exp (log 1 * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : z = 0
⊢ 0 = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : ¬z = 0
⊢ 0 = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : ¬y * z = 0
h✝¹ : ¬y = 0
h✝ : ¬0 = 0
⊢ 0 = exp (log 0 * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝² : ¬x = 0
h✝¹ : exp (log x * y) = 0
h✝ : z = 0
⊢ exp (log x * (y * z)) = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝² : ¬x = 0
h✝¹ : exp (log x * y) = 0
h✝ : ¬z = 0
⊢ exp (log x * (y * z)) = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝¹ : ¬x = 0
h✝ : ¬exp (log x * y) = 0
⊢ exp (log x * (y * z)) = exp (log (exp (log x * y)) * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
x y : ℂ
⊢ x ^ (-y) = (x ^ y)⁻¹
[PROOFSTEP]
simp only [cpow_def, neg_eq_zero, mul_neg]
[GOAL]
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else exp (-(log x * y))) =
    (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y))⁻¹
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 1⁻¹
[PROOFSTEP]
simp [exp_neg]
[GOAL]
case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹
[PROOFSTEP]
simp [exp_neg]
[GOAL]
case neg
x y : ℂ
h✝ : ¬x = 0
⊢ exp (-(log x * y)) = (exp (log x * y))⁻¹
[PROOFSTEP]
simp [exp_neg]
[GOAL]
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z
[PROOFSTEP]
rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]
[GOAL]
x : ℂ
⊢ x ^ (-1) = x⁻¹
[PROOFSTEP]
simpa using cpow_neg x 1
[GOAL]
x : ℂ
⊢ x ^ ↑0 = x ^ 0
[PROOFSTEP]
simp
[GOAL]
x : ℂ
n : ℕ
hx : x = 0
⊢ x ^ ↑(n + 1) = x ^ (n + 1)
[PROOFSTEP]
simp only [hx, pow_succ, Complex.zero_cpow (Nat.cast_ne_zero.2 (Nat.succ_ne_zero _)), zero_mul]
[GOAL]
x : ℂ
n : ℕ
hx : ¬x = 0
⊢ x ^ ↑(n + 1) = x ^ (n + 1)
[PROOFSTEP]
simp [cpow_add, hx, pow_add, cpow_nat_cast x n]
[GOAL]
x : ℂ
⊢ x ^ 2 = x ^ 2
[PROOFSTEP]
rw [← cpow_nat_cast]
[GOAL]
x : ℂ
⊢ x ^ 2 = x ^ ↑2
[PROOFSTEP]
simp only [Nat.cast_ofNat]
[GOAL]
x : ℂ
n : ℕ
⊢ x ^ ↑↑n = x ^ ↑n
[PROOFSTEP]
simp
[GOAL]
x : ℂ
n : ℕ
⊢ x ^ ↑-[n+1] = x ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc]
[GOAL]
x : ℂ
n : ℕ
⊢ x ^ ↑-[n+1] = (x ^ (n + 1))⁻¹
[PROOFSTEP]
simp only [Int.negSucc_coe, Int.cast_neg, Complex.cpow_neg, inv_eq_one_div, Int.cast_ofNat, cpow_nat_cast]
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
[PROOFSTEP]
suffices im (log x * (n⁻¹ : ℂ)) ∈ Ioc (-π) π
  by
  rw [← cpow_nat_cast, ← cpow_mul _ this.1 this.2, inv_mul_cancel, cpow_one]
  exact_mod_cast hn
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
this : (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
⊢ (x ^ (↑n)⁻¹) ^ n = x
[PROOFSTEP]
rw [← cpow_nat_cast, ← cpow_mul _ this.1 this.2, inv_mul_cancel, cpow_one]
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
this : (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
⊢ ↑n ≠ 0
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
[PROOFSTEP]
rw [mul_comm, ← ofReal_nat_cast, ← ofReal_inv, ofReal_mul_im, ← div_eq_inv_mul]
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
[PROOFSTEP]
rw [← pos_iff_ne_zero] at hn
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
[PROOFSTEP]
have hn' : 0 < (n : ℝ) := by assumption_mod_cast
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
⊢ 0 < ↑n
[PROOFSTEP]
assumption_mod_cast
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
[PROOFSTEP]
have hn1 : 1 ≤ (n : ℝ) := by exact_mod_cast Nat.succ_le_iff.2 hn
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ 1 ≤ ↑n
[PROOFSTEP]
exact_mod_cast Nat.succ_le_iff.2 hn
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
[PROOFSTEP]
constructor
[GOAL]
case left
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ -π < (log x).im / ↑n
[PROOFSTEP]
rw [lt_div_iff hn']
[GOAL]
case left
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ -π * ↑n < (log x).im
[PROOFSTEP]
calc
  -π * n ≤ -π * 1 := mul_le_mul_of_nonpos_left hn1 (neg_nonpos.2 Real.pi_pos.le)
  _ = -π := (mul_one _)
  _ < im (log x) := neg_pi_lt_log_im _
[GOAL]
case right
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im / ↑n ≤ π
[PROOFSTEP]
rw [div_le_iff hn']
[GOAL]
case right
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im ≤ π * ↑n
[PROOFSTEP]
calc
  im (log x) ≤ π := log_im_le_pi _
  _ = π * 1 := (mul_one π).symm
  _ ≤ π * n := mul_le_mul_of_nonneg_left hn1 Real.pi_pos.le
[GOAL]
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
rcases eq_or_ne r 0 with (rfl | hr)
[GOAL]
case inl
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (↑a * ↑b) ^ 0 = ↑a ^ 0 * ↑b ^ 0
[PROOFSTEP]
simp only [cpow_zero, mul_one]
[GOAL]
case inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
rcases eq_or_lt_of_le ha with (rfl | ha')
[GOAL]
case inr.inl
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : 0 ≤ 0
⊢ (↑0 * ↑b) ^ r = ↑0 ^ r * ↑b ^ r
[PROOFSTEP]
rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]
[GOAL]
case inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
rcases eq_or_lt_of_le hb with (rfl | hb')
[GOAL]
case inr.inr.inl
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : 0 ≤ 0
⊢ (↑a * ↑0) ^ r = ↑a ^ r * ↑0 ^ r
[PROOFSTEP]
rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]
[GOAL]
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
have ha'' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha'.ne'
[GOAL]
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
have hb'' : (b : ℂ) ≠ 0 := ofReal_ne_zero.mpr hb'.ne'
[GOAL]
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
hb'' : ↑b ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha, add_mul, exp_add, ←
  cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
[GOAL]
x n : ℂ
⊢ x⁻¹ ^ n = if arg x = π then ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹
[PROOFSTEP]
simp_rw [Complex.cpow_def, log_inv_eq_ite, inv_eq_zero, map_eq_zero, ite_mul, neg_mul, IsROrC.conj_inv, apply_ite conj,
  apply_ite exp, apply_ite Inv.inv, map_zero, map_one, exp_neg, inv_one, inv_zero, ← exp_conj, map_mul, conj_conj]
[GOAL]
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if arg x = π then (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹ else (exp (log x * n))⁻¹) =
    if arg x = π then if x = 0 then if n = 0 then 1 else 0 else (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (exp (log x * n))⁻¹
[PROOFSTEP]
split_ifs with hx hn ha ha
[GOAL]
case pos
x n : ℂ
hx : x = 0
hn : n = 0
ha : arg x = π
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hx : x = 0
hn : n = 0
ha : ¬arg x = π
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case pos
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : arg x = π
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : ¬arg x = π
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case pos
x n : ℂ
hx : ¬x = 0
h✝ : arg x = π
⊢ (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹ = (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hx : ¬x = 0
h✝ : ¬arg x = π
⊢ (exp (log x * n))⁻¹ = (exp (log x * n))⁻¹
[PROOFSTEP]
rfl
[GOAL]
x n : ℂ
hx : arg x ≠ π
⊢ x⁻¹ ^ n = (x ^ n)⁻¹
[PROOFSTEP]
rw [inv_cpow_eq_ite, if_neg hx]
[GOAL]
x n : ℂ
⊢ (x ^ n)⁻¹ = if arg x = π then ↑(starRingEnd ℂ) (x⁻¹ ^ ↑(starRingEnd ℂ) n) else x⁻¹ ^ n
[PROOFSTEP]
rw [inv_cpow_eq_ite, apply_ite conj, conj_conj, conj_conj]
[GOAL]
x n : ℂ
⊢ (x ^ n)⁻¹ =
    if arg x = π then if arg x = π then (x ^ n)⁻¹ else ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
x n : ℂ
h : arg x = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
h : ¬arg x = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n
[PROOFSTEP]
rw [inv_cpow _ _ h]
[GOAL]
x n : ℂ
⊢ ↑(starRingEnd ℂ) x ^ n = if arg x = π then x ^ n else ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)
[PROOFSTEP]
simp_rw [cpow_def, map_eq_zero, apply_ite conj, map_one, map_zero, ← exp_conj, map_mul, conj_conj, log_conj_eq_ite]
[GOAL]
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else exp ((if arg x = π then log x else ↑(starRingEnd ℂ) (log x)) * n)) =
    if arg x = π then if x = 0 then if n = 0 then 1 else 0 else exp (log x * n)
    else if x = 0 then if n = 0 then 1 else 0 else exp (↑(starRingEnd ℂ) (log x) * n)
[PROOFSTEP]
split_ifs with hcx hn hx
[GOAL]
case pos
x n : ℂ
hcx : x = 0
hn : n = 0
hx : arg x = π
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hcx : x = 0
hn : n = 0
hx : ¬arg x = π
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case pos
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : arg x = π
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : ¬arg x = π
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case pos
x n : ℂ
hcx : ¬x = 0
h✝ : arg x = π
⊢ exp (log x * n) = exp (log x * n)
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hcx : ¬x = 0
h✝ : ¬arg x = π
⊢ exp (↑(starRingEnd ℂ) (log x) * n) = exp (↑(starRingEnd ℂ) (log x) * n)
[PROOFSTEP]
rfl
[GOAL]
x n : ℂ
hx : arg x ≠ π
⊢ ↑(starRingEnd ℂ) x ^ n = ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)
[PROOFSTEP]
rw [conj_cpow_eq_ite, if_neg hx]
[GOAL]
x n : ℂ
hx : arg x ≠ π
⊢ x ^ ↑(starRingEnd ℂ) n = ↑(starRingEnd ((fun x => ℂ) x)) (↑(starRingEnd ℂ) x ^ n)
[PROOFSTEP]
rw [conj_cpow _ _ hx, conj_conj]


[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]