α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < dValue N
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
⊢ 0 < dValue N
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (succ_pos'.trans_le hN₃)
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ log 2 * ↑(nValue N) ≤ log ↑N

α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑(nValue N)

α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑N ^ (1 / ↑(nValue N)) ≠ 0

α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑N ^ (1 / ↑(nValue N)) / 2
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < dValue N
rw [dValue, floor_pos, ← log_le_log zero_lt_one, log_one, log_div _ two_ne_zero, log_rpow hN₀,
  div_mul_eq_mul_div, one_mul, sub_nonneg, le_div_iff]
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 2 * ↑(nValue N) ≤ log ↑N
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ log 2 * ↑(nValue N) ≤ log ↑N
have : (nValue N : ℝ) ≤ 2 * sqrt (log N) := by
  apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
  rw [two_mul, add_le_add_iff_left]
  apply le_sqrt_of_sq_le
  rw [one_pow, le_log_iff_exp_le hN₀]
  exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 2 * (2 * Real.sqrt (log ↑N)) ≤ log ↑N
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 2 * ↑(nValue N) ≤ log ↑N
apply (mul_le_mul_of_nonneg_left this <| log_nonneg one_le_two).trans _
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 2 * 2 ≤ Real.sqrt (log ↑N)

α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 1 < N
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 2 * (2 * Real.sqrt (log ↑N)) ≤ log ↑N
rw [← mul_assoc, ← le_div_iff (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _), div_sqrt]
no goals
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 1 < N
exact hN₃.trans_lt' (by norm_num)
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ Real.sqrt (log ↑N) + 1 ≤ 2 * Real.sqrt (log ↑N)
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ≤ Real.sqrt (log ↑N)
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ Real.sqrt (log ↑N) + 1 ≤ 2 * Real.sqrt (log ↑N)
rw [two_mul, add_le_add_iff_left]
case h
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ^ 2 ≤ log ↑N
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ≤ Real.sqrt (log ↑N)
apply le_sqrt_of_sq_le
case h
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ exp 1 ≤ ↑N
case h
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ^ 2 ≤ log ↑N
rw [one_pow, le_log_iff_exp_le hN₀]
no goals
case h
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ exp 1 ≤ ↑N
exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)
no goals
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 2.7182818286 ≤ ↑8
norm_num
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ Real.sqrt (log 8) ≤ Real.sqrt (log ↑N)
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 2 * 2 ≤ Real.sqrt (log ↑N)
apply log_two_mul_two_le_sqrt_log_eight.trans
case h
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 8 ≤ log ↑N
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ Real.sqrt (log 8) ≤ Real.sqrt (log ↑N)
apply Real.sqrt_le_sqrt
case h
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 8 ≤ ↑N

α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 0 < 8
case h
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 8 ≤ log ↑N
rw [log_le_log _ hN₀]
no goals
case h
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 8 ≤ ↑N
exact_mod_cast hN₃
no goals
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 0 < 8
norm_num
no goals
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 1 < 8
norm_num
no goals
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑(nValue N)
exact cast_pos.2 (nValue_pos <| hN₃.trans' <| by norm_num)
no goals
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 2 ≤ 8
norm_num
no goals
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑N ^ (1 / ↑(nValue N)) ≠ 0
exact (rpow_pos_of_pos hN₀ _).ne'
no goals
α : Type ?u.742881
β : Type ?u.742884
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑N ^ (1 / ↑(nValue N)) / 2
exact div_pos (rpow_pos_of_pos hN₀ _) zero_lt_two