BKLNW.f_crude_le
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:259 to 276
Source documentation
Given coefficient upper bounds and the two endpoint values of the majorant under 291.60,
the exact Lemma-8 supremum for any row [b,b'] (k=5, 20 ≤ b) is ≤ T. -/
theorem row_bound_k5 (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 : Gp A₁ A₂ E b ≤ T) (hGb' : Gp A₁ A₂ E b' ≤ T) :
B_8_exact 5 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 hy5 : (0 : ℝ) ≤ y ^ 5 := pow_nonneg hy0 5
have hconv : Gp A₁ A₂ E y ≤ T :=
le_trans ((Gp_convexOn b b' hbb' hb20 hA1 hA2 hE).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]
have e1 : (0 : ℝ) ≤ y ^ 5 * Real.exp (-(1 / 2 * y)) := mul_nonneg hy5 (Real.exp_pos _).le
have e2 : (0 : ℝ) ≤ y ^ 5 * Real.exp (-(2 / 3 * y)) := mul_nonneg hy5 (Real.exp_pos _).le
have h1 : Inputs.default.a₁ b * y ^ 5 * Real.exp (-(1 / 2 * y)) ≤ A₁ * (y ^ 5 * 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 ^ 5 * Real.exp (-(2 / 3 * y)) ≤ A₂ * (y ^ 5 * Real.exp (-(2 / 3 * y))) := by
rw [mul_assoc]; exact mul_le_mul_of_nonneg_right ha2 e2
have h3 : Inputs.default.ε b * y ^ 5 ≤ E * y ^ 5 := mul_le_mul_of_nonneg_right heps hy5
have hGpy : Gp A₁ A₂ E y
= A₁ * (y ^ 5 * Real.exp (-(1 / 2 * y))) + A₂ * (y ^ 5 * Real.exp (-(2 / 3 * y))) + E * y ^ 5 := by
unfold Gp expT; ring
rw [hGpy] at hconv
linarith [h1, h2, h3, hconv]
/-! Cert-free crude a₂ bound + regime-2 row 60 (b'=65, crude a₂, convexity template).
Exact Lean statement
lemma f_crude_le (x : ℝ) (hx : 1 ≤ x) : f x ≤ (⌊log x / log 2⌋₊ : ℝ)
Complete declaration
Lean source
lemma f_crude_le (x : ℝ) (hx : 1 ≤ x) : f x ≤ (⌊log x / log 2⌋₊ : ℝ) := by have hcard : ((Finset.Icc 3 ⌊log x / log 2⌋₊).card : ℝ) ≤ (⌊log x / log 2⌋₊ : ℝ) := by rw [Nat.card_Icc] have h : ⌊log x / log 2⌋₊ + 1 - 3 ≤ ⌊log x / log 2⌋₊ := by omega exact_mod_cast h unfold f calc ∑ k ∈ Finset.Icc 3 ⌊log x / log 2⌋₊, x ^ (1 / (k : ℝ) - 1 / 3) ≤ ∑ _k ∈ Finset.Icc 3 ⌊log x / log 2⌋₊, (1 : ℝ) := by apply Finset.sum_le_sum intro k hk have hk3 : 3 ≤ k := (Finset.mem_Icc.mp hk).1 apply Real.rpow_le_one_of_one_le_of_nonpos hx have hkr : (3 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk3 have : (1 : ℝ) / (k : ℝ) ≤ 1 / 3 := one_div_le_one_div_of_le (by norm_num) hkr linarith _ = ((Finset.Icc 3 ⌊log x / log 2⌋₊).card : ℝ) := by rw [Finset.sum_const, nsmul_eq_mul, mul_one] _ ≤ (⌊log x / log 2⌋₊ : ℝ) := hcard