-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem bound (hN : 4096 ≤ N) : (N : ℝ) ^ (nValue N : ℝ)⁻¹ / exp 1 < dValue N

Proof state:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 1 ≤ ↑N

Tactic:
rw [one_le_cast]

Result:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 1 ≤ N

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / (1.38 * √(log ↑N))

Tactic:
rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]

Result:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * 1.38 ≤ √(log ↑N)

N : ℕ
hN : 4096 ≤ N
⊢ 0 < 1.38

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 1 < ↑N

Tactic:
rw [one_lt_cast]

Result:
N : ℕ
hN : 4096 ≤ N
⊢ 1 < N

Proof state:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 1 ≤ N

Tactic:
exact hN.trans' (by norm_num1)

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * 1.38 ≤ √(log ↑N)

Tactic:
norm_num

Result:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log ↑N)

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ 0.6931471803

Tactic:
norm_num1

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / rexp 1) ≤ ↑N ^ (↑(nValue N))⁻¹

Tactic:
rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv]

Result:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / ↑(nValue N)

case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N

case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

case h₁
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / ↑(nValue N)

Tactic:
apply le_trans _ (div_le_div_of_nonneg_left _ _ (ceil_lt_mul _).le)

Result:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / (1.38 * √(log ↑N))

N : ℕ
hN : 4096 ≤ N
⊢ 0 ≤ log ↑N

N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈√(log ↑N)⌉₊

N : ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ √(log ↑N)

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log ↑N)

Tactic:
exact le_sqrt_log hN

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 1 < N

Tactic:
exact hN.trans_lt' (by norm_num1)

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 2 ≤ 2.7182818283

Tactic:
norm_num1

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈√(log ↑N)⌉₊

Tactic:
rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]

Result:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < log ↑N

Proof state:
case h
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < ↑12

Tactic:
norm_num1

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ ↑12 * log 2 ≤ log ↑N

Tactic:
rw [← log_rpow zero_lt_two, rpow_natCast]

Result:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 ^ 12) ≤ log ↑N

Proof state:
case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 1 - 2 / rexp 1

Tactic:
rw [sub_pos, div_lt_one (exp_pos _)]

Result:
case h
N : ℕ
hN : 4096 ≤ N
⊢ 2 < rexp 1

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ ↑N ^ (↑(nValue N))⁻¹ / rexp 1 < ↑(dValue N)

Tactic:
apply div_lt_floor _

Result:
N : ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / rexp 1) ≤ ↑N ^ (↑(nValue N))⁻¹

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 1.38

Tactic:
norm_num1

Result:
no goals

Proof state:
case h
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ log ↑N

Tactic:
refine le_trans ?_ this

Result:
case h
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ ↑12 * log 2

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 1 < 4096

Tactic:
norm_num1

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ √(log ↑N)

Tactic:
apply le_sqrt_of_sq_le

Result:
case h
N : ℕ
hN : 4096 ≤ N
⊢ (50 / 19) ^ 2 ≤ log ↑N

Proof state:
case h
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ log 2

Tactic:
exact log_two_gt_d9.le.trans' (by norm_num1)

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 4096

Tactic:
norm_num1

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 ^ 12

Tactic:
positivity

Result:
no goals

Proof state:
case h
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ ↑12 * log 2

Tactic:
rw [← div_le_iff₀']

Result:
case h
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ log 2

case h
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < ↑12

Proof state:
case h
N : ℕ
hN : 4096 ≤ N
⊢ (50 / 19) ^ 2 ≤ log ↑N

Tactic:
have : (12 : ℕ) * log 2 ≤ log N := by
  rw [← log_rpow zero_lt_two, rpow_natCast]
  exact log_le_log (by positivity) (mod_cast hN)

Result:
case h
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ log ↑N

Proof state:
case h₁
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
case h
N : ℕ
hN : 4096 ≤ N
⊢ 2 < rexp 1

Tactic:
exact lt_of_le_of_lt (by norm_num1) exp_one_gt_d9

Result:
no goals

Proof state:
case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

Tactic:
refine div_pos zero_lt_two ?_

Result:
case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 1 - 2 / rexp 1

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 0 ≤ log ↑N

Tactic:
apply log_nonneg

Result:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 1 ≤ ↑N

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 1 ≤ 4096

Tactic:
norm_num1

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 ^ 12) ≤ log ↑N

Tactic:
exact log_le_log (by positivity) (mod_cast hN)

Result:
no goals

Proof state:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < N

Tactic:
exact hN.trans_lt' (by norm_num1)

Result:
no goals

Proof state:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N

Tactic:
rw [cast_pos]

Result:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < N

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < log ↑N

Tactic:
refine log_pos ?_

Result:
N : ℕ
hN : 4096 ≤ N
⊢ 1 < ↑N