Source indexedtheorem · leanprover/lean4:v4.32.0

BKLNW.row_bound_k1

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:496 to 531

Source documentation

k = 1 row template (majorant y·e^{-cy}, no pow machinery): given coefficient upper bounds and the two endpoint majorant values under T, the exact Lemma-8 supremum for any row [b,b'] (20 ≤ b) is ≤ T.

Exact Lean statement

theorem row_bound_k1 (b b' A₁ A₂ E T : ℝ)
    (hbb' : b ≤ b') (hb20 : 20 ≤ 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)
    (hGb : G1 A₁ A₂ E b ≤ T) (hGb' : G1 A₁ A₂ E b' ≤ T) :
    B_8_exact 1 b b' ≤ T

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem row_bound_k1 (b b' A₁ A₂ E T : ℝ)    (hbb' : b ≤ b') (hb20 : 20 ≤ 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)    (hGb : G1 A₁ A₂ E b ≤ T) (hGb' : G1 A₁ A₂ E b' ≤ T) :    B_8_exact 1 b b' ≤ T := by  unfold B_8_exact  refine B_le_of_forall_log _ _ _ _ hbb' ?_  intro y hy  have hy0 : (0 : ℝ) ≤ y := by have := hy.1; linarith  have hconv : G1 A₁ A₂ E y ≤ T :=    le_trans ((G1_convexOn b b' hbb' hb20 hA1 hA2).le_max_of_mem_Icc      (left_mem_Icc.mpr hbb') (right_mem_Icc.mpr hbb') hy) (max_le hGb hGb')  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]  simp only [pow_one]  have e1 : (0 : ℝ) ≤ y * Real.exp (-(1 / 2 * y)) := mul_nonneg hy0 (Real.exp_pos _).le  have e2 : (0 : ℝ) ≤ y * Real.exp (-(2 / 3 * y)) := mul_nonneg hy0 (Real.exp_pos _).le  have h1 : Inputs.default.a₁ b * y * Real.exp (-(1 / 2 * y)) ≤ A₁ * (y * Real.exp (-(1 / 2 * y))) := by    rw [mul_assoc]; exact mul_le_mul_of_nonneg_right ha1 e1  have h2 : Inputs.default.a₂ b * y * Real.exp (-(2 / 3 * y)) ≤ A₂ * (y * Real.exp (-(2 / 3 * y))) := by    rw [mul_assoc]; exact mul_le_mul_of_nonneg_right ha2 e2  have h3 : Inputs.default.ε b * y ≤ E * y := mul_le_mul_of_nonneg_right heps hy0  have hG1y : G1 A₁ A₂ E y      = A₁ * (y * Real.exp (-(1 / 2 * y))) + A₂ * (y * Real.exp (-(2 / 3 * y))) + E * y := by    unfold G1 eT; ring  rw [hG1y] at hconv  linarith [h1, h2, h3, hconv]