Source indexedtheorem · leanprover/lean4:v4.32.0

BKLNW.row_bound_kge2

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:642 to 680

Source documentation

General-k (k = m+2, m ≤ 3) row template: 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. Proven ONCE; rows 20-... for every column k ∈ {2,3,4,5} instantiate it.

Exact Lean statement

theorem row_bound_kge2 (m : ℕ) (hm : m ≤ 3) (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)
    (hPb : Pp m A₁ A₂ E b ≤ T) (hPb' : Pp m A₁ A₂ E b' ≤ T) :
    B_8_exact (m + 2) b b' ≤ T

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem row_bound_kge2 (m : ℕ) (hm : m ≤ 3) (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)    (hPb : Pp m A₁ A₂ E b ≤ T) (hPb' : Pp m A₁ A₂ E b' ≤ T) :    B_8_exact (m + 2) 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 hyk : (0 : ℝ) ≤ y ^ (m + 2) := pow_nonneg hy0 (m + 2)  have hconv : Pp m A₁ A₂ E y ≤ T :=    le_trans ((Pp_convexOn m b b' hbb' hb20 hm hA1 hA2 hE).le_max_of_mem_Icc      (left_mem_Icc.mpr hbb') (right_mem_Icc.mpr hbb') hy) (max_le hPb hPb')  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 e1 : (0 : ℝ) ≤ y ^ (m + 2) * Real.exp (-(1 / 2 * y)) := mul_nonneg hyk (Real.exp_pos _).le  have e2 : (0 : ℝ) ≤ y ^ (m + 2) * Real.exp (-(2 / 3 * y)) := mul_nonneg hyk (Real.exp_pos _).le  have h1 : Inputs.default.a₁ b * y ^ (m + 2) * Real.exp (-(1 / 2 * y))      ≤ A₁ * (y ^ (m + 2) * 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 ^ (m + 2) * Real.exp (-(2 / 3 * y))      ≤ A₂ * (y ^ (m + 2) * Real.exp (-(2 / 3 * y))) := by    rw [mul_assoc]; exact mul_le_mul_of_nonneg_right ha2 e2  have h3 : Inputs.default.ε b * y ^ (m + 2) ≤ E * y ^ (m + 2) := mul_le_mul_of_nonneg_right heps hyk  have hPy : Pp m A₁ A₂ E y      = A₁ * (y ^ (m + 2) * Real.exp (-(1 / 2 * y))) + A₂ * (y ^ (m + 2) * Real.exp (-(2 / 3 * y)))          + E * y ^ (m + 2) := by    unfold Pp pT; ring  rw [hPy] at hconv  linarith [h1, h2, h3, hconv]