α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ Real.sqrt (log 8)
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
⊢ log 2 * 2 ≤ Real.sqrt (log 8)
have : (8 : ℝ) = 2 ^ ((3 : ℕ) : ℝ) := by rw [rpow_nat_cast]; norm_num
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ Real.sqrt (↑3 * log 2)
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ Real.sqrt (log 8)
rw [this, log_rpow zero_lt_two (3 : ℕ)]
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ (log 2 * 2) ^ 2 ≤ ↑3 * log 2
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ Real.sqrt (↑3 * log 2)
apply le_sqrt_of_sq_le
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 * log 2 ≤ ↑3 * log 2
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ (log 2 * 2) ^ 2 ≤ ↑3 * log 2
rw [mul_pow, sq (log 2), mul_assoc, mul_comm]
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 ≤ ↑3
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 * log 2 ≤ ↑3 * log 2
refine' mul_le_mul_of_nonneg_right _ (log_nonneg one_le_two)
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 ≤ ↑3 / 2 ^ 2

case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 ≤ ↑3
rw [← le_div_iff]
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0.6931471808 ≤ ↑3 / 2 ^ 2

case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 ≤ ↑3 / 2 ^ 2

case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2
apply log_two_lt_d9.le.trans
no goals
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0.6931471808 ≤ ↑3 / 2 ^ 2

case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2
all_goals norm_num1
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
⊢ 8 = 2 ^ 3
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
⊢ 8 = 2 ^ ↑3
rw [rpow_nat_cast]
no goals
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
⊢ 8 = 2 ^ 3
norm_num
no goals
case h
α : Type ?u.611385
β : Type ?u.611388
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2
norm_num1