α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / exp 1) ≤ ↑N ^ (1 / ↑(nValue N))
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ ↑N ^ (1 / ↑(nValue N)) / exp 1 < ↑(dValue N)
apply div_lt_floor _
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) ≤ log ↑N / ↑(nValue N)

case hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N

case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / exp 1)

case h₁
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (1 / ↑(nValue N))
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / exp 1) ≤ ↑N ^ (1 / ↑(nValue N))
rw [← log_le_log, log_rpow, mul_comm, ← div_eq_mul_one_div]
case h₁.hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
case h₁
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (1 / ↑(nValue N))
apply rpow_pos_of_pos
case h₁.hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
case h₁.hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
rw [cast_pos]
no goals
case h₁.hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
exact hN.trans_lt' (by norm_num1)
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) ≤ log ↑N / (1.38 * Real.sqrt (log ↑N))

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 ≤ log ↑N

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈Real.sqrt (log ↑N)⌉₊

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ Real.sqrt (log ↑N)
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) ≤ log ↑N / ↑(nValue N)
apply le_trans _ (div_le_div_of_le_left _ _ (ceil_lt_mul _).le)
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) * 1.38 ≤ Real.sqrt (log ↑N)

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 1.38

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 ≤ log ↑N

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈Real.sqrt (log ↑N)⌉₊

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ Real.sqrt (log ↑N)
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) ≤ log ↑N / (1.38 * Real.sqrt (log ↑N))

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 ≤ log ↑N

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈Real.sqrt (log ↑N)⌉₊

α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ Real.sqrt (log ↑N)
rw [mul_comm, ← div_div, div_sqrt, le_div_iff]
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ (50 / 19) ^ 2 ≤ log ↑N
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ Real.sqrt (log ↑N)
apply le_sqrt_of_sq_le
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ ↑12 * log 2
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ log ↑N
refine' le_trans _ this
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ ↑12 * log 2
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ ↑12 * log 2
simp only [cast_one]
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ log 2

case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < ↑12
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ ↑12 * log 2
rw [← div_le_iff']
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) * (69 / 50) ≤ Real.sqrt (log ↑N)
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) * 1.38 ≤ Real.sqrt (log ↑N)
norm_num
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) * (69 / 50) ≤ Real.sqrt (log ↑N)
exact le_sqrt_log hN
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 1.38
norm_num1
case hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 ≤ ↑N
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 ≤ log ↑N
apply log_nonneg
case hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 ≤ N
case hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 ≤ ↑N
rw [one_le_cast]
no goals
case hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 ≤ N
exact hN.trans' (by norm_num1)
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 ≤ 4096
norm_num1
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < log ↑N
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈Real.sqrt (log ↑N)⌉₊
rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 < ↑N
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < log ↑N
refine' log_pos _
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 < N
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 < ↑N
rw [one_lt_cast]
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 < N
exact hN.trans_lt' (by norm_num1)
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 < 4096
norm_num1
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 ^ 12 ≤ ↑N

case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 2 ^ ↑12

case h₁
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ ↑12 * log 2 ≤ log ↑N
rw [← log_rpow zero_lt_two, log_le_log, rpow_nat_cast]
case h₁
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
case h₁
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
rw [cast_pos]
no goals
case h₁
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
exact hN.trans_lt' (by norm_num1)
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 4096 ≤ ↑N
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 ^ 12 ≤ ↑N
norm_num1
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 4096 ≤ ↑N
exact_mod_cast hN
no goals
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 2 ^ ↑12
exact rpow_pos_of_pos zero_lt_two _
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 4096
norm_num1
no goals
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ log 2
exact log_two_gt_d9.le.trans' (by norm_num1)
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ 0.6931471803
norm_num1
no goals
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < ↑12
norm_num1
case hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
case hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
rw [cast_pos]
no goals
case hx
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
exact hN.trans_lt' (by norm_num1)
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 4096
norm_num1
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 1 - 2 / exp 1
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / exp 1)
refine' div_pos zero_lt_two _
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 < exp 1
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 1 - 2 / exp 1
rw [sub_pos, div_lt_one (exp_pos _)]
no goals
case h
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 < exp 1
exact lt_of_le_of_lt (by norm_num1) exp_one_gt_d9
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 ≤ 2.7182818283
norm_num1
no goals
α : Type ?u.786208
β : Type ?u.786211
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 4096
norm_num1