FKS2.BKLNW_a1_le_two_of_ge_1000

lemma BKLNW_a1_le_two_of_ge_1000 (t : ℝ) (ht : t ≥ 1000) :    BKLNW.a₁ t ≤ 2 := by  -- Sketch:  -- unfold `BKLNW.a₁` -> `Inputs.default.a₁`.  -- split on `t ≤ 2*log x₁`; in either branch it is `1 + ε(...)` with ε tiny.  -- For the branch `1 + table_8_ε (t/2)`, use:  --   `BKLNW_app.table_8_ε_le_of_row (b₀ := 20) (ε := 4.2676e-5) ...`  -- because `20 ≤ t/2` when `t ≥ 1000`.  -- conclude by `linarith` / `nlinarith`.  have h_exp20 : exp (20 : ℝ) ≤ (1e19 : ℝ) := by    grw [← exp_one_rpow 20, Real.exp_one_lt_d9]    norm_num only  have h20_log : (20 : ℝ) ≤ log (1e19 : ℝ) := by    have := log_le_log (exp_pos (20 : ℝ)) h_exp20    simpa [log_exp] using this  have hmain :      (if t ≤ 2 * log (1e19 : ℝ) then 1 + BKLNW_app.table_8_ε (log (1e19 : ℝ))       else 1 + BKLNW_app.table_8_ε (t / 2)) ≤ 2 := by    by_cases hif : t ≤ 2 * log (1e19 : ℝ)    · have h_eps : BKLNW_app.table_8_ε (log (1e19 : ℝ)) ≤ 4.2676e-5 := by        exact BKLNW_app.table_8_ε_le_of_row          (b₀ := 20) (ε := 4.2676e-5) BKLNW_app.table_8_mem_20 h20_log      simp [hif]      linarith    · have h20 : (20 : ℝ) ≤ t / 2 := by linarith [ht]      have h_eps : BKLNW_app.table_8_ε (t / 2) ≤ 4.2676e-5 := by        exact BKLNW_app.table_8_ε_le_of_row          (b₀ := 20) (ε := 4.2676e-5) BKLNW_app.table_8_mem_20 h20      simp [hif]      linarith  simpa [BKLNW.a₁, BKLNW.Inputs.a₁, BKLNW.Inputs.default, BKLNW.Pre_inputs.default] using hmain