case inl
α : Type ?u.881020
β : Type ?u.881023
n d k : ℕ
x : Fin n → ℕ
hN : 1 ≤ 1
hN' : 1 ≤ 4096
⊢ ↑1 * exp (-4 * Real.sqrt (log ↑1)) ≤ 1

case inr
α : Type ?u.881020
β : Type ?u.881023
n d k N : ℕ
x : Fin n → ℕ
hN✝ : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ 1
α : Type ?u.881020
β : Type ?u.881023
n d k N : ℕ
x : Fin n → ℕ
hN : 1 ≤ N
hN' : N ≤ 4096
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ 1
obtain rfl | hN := hN.eq_or_lt
no goals
case inl
α : Type ?u.881020
β : Type ?u.881023
n d k : ℕ
x : Fin n → ℕ
hN : 1 ≤ 1
hN' : 1 ≤ 4096
⊢ ↑1 * exp (-4 * Real.sqrt (log ↑1)) ≤ 1
norm_num
no goals
case inr
α : Type ?u.881020
β : Type ?u.881023
n d k N : ℕ
x : Fin n → ℕ
hN✝ : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ 1
exact lower_bound_le_one' hN hN'