α : Type ?u.840499
β : Type ?u.840502
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ exp (4 ^ 2)
α : Type ?u.840499
β : Type ?u.840502
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ 1
rw [← log_le_log (mul_pos (cast_pos.2 (zero_lt_two.trans_le hN)) (exp_pos _)) zero_lt_one,
  log_one, log_mul (cast_pos.2 (zero_lt_two.trans_le hN)).ne' (exp_pos _).ne', log_exp, neg_mul, ←
  sub_eq_add_neg, sub_nonpos, ←
  div_le_iff (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 <| one_lt_two.trans_le hN), div_sqrt,
  sqrt_le_left zero_le_four, log_le_iff_le_exp (cast_pos.2 (zero_lt_two.trans_le hN))]
α : Type ?u.840499
β : Type ?u.840502
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ exp 16
α : Type ?u.840499
β : Type ?u.840502
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ exp (4 ^ 2)
norm_num1
α : Type ?u.840499
β : Type ?u.840502
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ 4096
α : Type ?u.840499
β : Type ?u.840502
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ exp 16
apply le_trans _ four_zero_nine_six_lt_exp_sixteen.le
no goals
α : Type ?u.840499
β : Type ?u.840502
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ 4096
exact_mod_cast hN'