BKLNW.row_bound_pointwise
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:706 to 745
Source documentation
General a₁ bound on the constant branch: valid for every b ≤ 86. -/
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']
/-! ## Regime-3 pointwise template (b ≳ 80): no convexity, no derivative machinery,
uniform in every column k. Per-term endpoint bounds reduce the supremum to ONE
constant inequality, dischargeable by interval_decide per row. Ported from the
compiled row100_pointwise.lean exemplar, parameterized over k + coefficients.
Exact Lean statement
theorem row_bound_pointwise (k : ℕ) (b b' A₁ A₂ E T : ℝ)
(hbb' : b ≤ b') (hb0 : 0 ≤ b)
(hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) (hE : 0 ≤ E)
(ha1 : Inputs.default.a₁ b ≤ A₁) (ha2 : Inputs.default.a₂ b ≤ A₂)
(heps : Inputs.default.ε b ≤ E)
(hT : A₁ * b' ^ k * Real.exp (-(1 / 2 * b)) + A₂ * b' ^ k * Real.exp (-(2 / 3 * b))
+ E * b' ^ k ≤ T) :
B_8_exact k b b' ≤ TComplete declaration
Lean source
theorem row_bound_pointwise (k : ℕ) (b b' A₁ A₂ E T : ℝ) (hbb' : b ≤ b') (hb0 : 0 ≤ b) (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) (hE : 0 ≤ E) (ha1 : Inputs.default.a₁ b ≤ A₁) (ha2 : Inputs.default.a₂ b ≤ A₂) (heps : Inputs.default.ε b ≤ E) (hT : A₁ * b' ^ k * Real.exp (-(1 / 2 * b)) + A₂ * b' ^ k * Real.exp (-(2 / 3 * b)) + E * b' ^ k ≤ T) : B_8_exact k b b' ≤ T := by have hb'0 : (0 : ℝ) ≤ b' := le_trans hb0 hbb' unfold B_8_exact refine B_le_of_forall_log _ _ _ _ hbb' ?_ intro y hy obtain ⟨hyb, hyb'⟩ := hy have hy0 : (0 : ℝ) ≤ y := le_trans hb0 hyb have hyk : (0 : ℝ) ≤ y ^ k := pow_nonneg hy0 k rw [show Finset.Icc 1 2 = {1, 2} from by decide, Finset.sum_insert (by decide), Finset.sum_singleton] have hif1 : (if (1 : ℕ) = 1 then Inputs.default.a₁ b else if (1 : ℕ) = 2 then Inputs.default.a₂ b else 0) = Inputs.default.a₁ b := by norm_num have hif2 : (if (2 : ℕ) = 1 then Inputs.default.a₁ b else if (2 : ℕ) = 2 then Inputs.default.a₂ b else 0) = Inputs.default.a₂ b := by norm_num have ce1 : Real.exp (-(((1 : ℕ) : ℝ) / (((1 : ℕ) : ℝ) + 1) * y)) = Real.exp (-(1 / 2 * y)) := by congr 1; push_cast; ring have ce2 : Real.exp (-(((2 : ℕ) : ℝ) / (((2 : ℕ) : ℝ) + 1) * y)) = Real.exp (-(2 / 3 * y)) := by congr 1; push_cast; ring rw [hif1, hif2, ce1, ce2] have hpow : y ^ k ≤ b' ^ k := by gcongr have ht1 : Inputs.default.a₁ b * y ^ k * Real.exp (-(1 / 2 * y)) ≤ A₁ * b' ^ k * Real.exp (-(1 / 2 * b)) := mul_le_mul (mul_le_mul ha1 hpow hyk hA1) (Real.exp_le_exp.mpr (by linarith)) (Real.exp_pos _).le (mul_nonneg hA1 (pow_nonneg hb'0 k)) have ht2 : Inputs.default.a₂ b * y ^ k * Real.exp (-(2 / 3 * y)) ≤ A₂ * b' ^ k * Real.exp (-(2 / 3 * b)) := mul_le_mul (mul_le_mul ha2 hpow hyk hA2) (Real.exp_le_exp.mpr (by linarith)) (Real.exp_pos _).le (mul_nonneg hA2 (pow_nonneg hb'0 k)) have ht3 : Inputs.default.ε b * y ^ k ≤ E * b' ^ k := mul_le_mul heps hpow hyk hE linarith [ht1, ht2, ht3, hT]