Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.a1_le_small

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:684 to 698

Source documentation

General a₁ bound on the constant branch: valid for every b ≤ 86.

Exact Lean statement

lemma a1_le_small {b : ℝ} (hb : b ≤ 86) : Inputs.default.a₁ b ≤ (1.00000002 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma a1_le_small {b : ℝ} (hb : b ≤ 86) : Inputs.default.a₁ b ≤ (1.00000002 : ℝ) := by  have hlog : (43 : ℝ) < log Inputs.default.x₁ ∧ log Inputs.default.x₁ < 44 := by    change (43 : ℝ) < log (1e19 : ℝ) ∧ log (1e19 : ℝ) < 44    have h1e19 : (1e19 : ℝ) = (10 : ℝ) ^ 19 := by norm_num    rw [h1e19, Real.log_pow]; push_cast    constructor <;> nlinarith [LogTables.log_10_gt, LogTables.log_10_lt]  have hε19 : Inputs.default.ε (log Inputs.default.x₁) ≤ 1.93378e-8 * BKLNW_app.table_8_margin := by    change BKLNW_app.table_8_ε (log Inputs.default.x₁) ≤ 1.93378e-8 * BKLNW_app.table_8_margin    grw [BKLNW_app.table_8_ε.le_simp (log Inputs.default.x₁) (by linarith [hlog.1])]    grind [BKLNW_app.table_8_ε']  unfold Inputs.a₁  rw [if_pos (by linarith [hlog.1] : b ≤ 2 * log Inputs.default.x₁)]  have hb' : (1.93378e-8 * BKLNW_app.table_8_margin : ℝ) ≤ 1.00000002 - 1 := by    norm_num [BKLNW_app.table_8_margin]  linarith [hε19, hb']