α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 < Real.sqrt (log ↑N)
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 3 ≤ nValue N
rw [nValue, ← lt_iff_add_one_le, lt_ceil, cast_two]
case h
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ 2 < log ↑N
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 < Real.sqrt (log ↑N)
apply lt_sqrt_of_sq_lt
case h
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log ↑N
case h
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ 2 < log ↑N
have : (2 : ℝ) ^ ((6 : ℕ) : ℝ) ≤ N := by
  rw [rpow_nat_cast]
  exact (cast_le.2 hN).trans' (by norm_num1)
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log (2 ^ ↑6)

α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑N
case h
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log ↑N
apply lt_of_lt_of_le _ ((log_le_log (rpow_pos_of_pos zero_lt_two _) _).2 this)
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 < log 2

α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑6

α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑N
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log (2 ^ ↑6)

α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑N
rw [log_rpow zero_lt_two, ← div_lt_iff']
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < N
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑N
rw [cast_pos]
no goals
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < N
exact hN.trans_lt' (by norm_num1)
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑N
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ ↑6 ≤ ↑N
rw [rpow_nat_cast]
no goals
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑N
exact (cast_le.2 hN).trans' (by norm_num1)
no goals
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑64
norm_num1
no goals
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 < log 2
exact log_two_gt_d9.trans_le' (by norm_num1)
no goals
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 ≤ 0.6931471803
norm_num1
no goals
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑6
norm_num1
no goals
α : Type ?u.740413
β : Type ?u.740416
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < 64
norm_num1