Source indexedtheorem · leanprover/lean4:v4.32.0

BKLNW.bklnw_eq_3_11

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1207 to 1252

Mathematical statement

Exact Lean statement

@[blueprint
  "bklnw-eq-3-11"
  (title := "BKLNW Equation (3.11)")
  (statement := /--  Let $k=1,\ldots,5$. Assume there exist a positive integer $n$, real numbers $a_{\ell} \ge 0$ for every $\ell \in \{1, 2, \ldots, n \}$.  Let $b' > b \geq 2k$. Then $B_k \leq \tilde B_k$ where
  $$ \tilde B_k := b^{k} \sum_{\ell=1}^n a_{\ell} \exp\left(-\frac{\ell b}{\ell+1}\right) + \varepsilon(b) (b')^k. $$
  . -/)
  (proof := /-- Observe that since $x\ge e^b > e^{2k} \ge e^{\frac{k(\ell+1)}{\ell}}$, then each $a_\ell (\log x)^k x^{-\frac{\ell}{\ell + 1}}$ decreases with $x$.  The claim follows since $\varepsilon(b) (\log x)^k$ increases with $x$.
 -/)
  (latexEnv := "sublemma")
  (discussion := 1253)]
theorem bklnw_eq_3_11 (k n : ℕ) (hk : 1 ≤ k) (a : ℕ → ℝ) (ε : ℝ → ℝ) (b b' : ℝ)
  (ha : ∀ ℓ ∈ Finset.Icc 1 n, 0 ≤ a ℓ)
  (hε : 0 ≤ ε b)
  (hbb : b < b') (hbk : b ≥ 2 * k) :
  B k n a ε b b' ≤ Btilde k n a ε b b'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "bklnw-eq-3-11"  (title := "BKLNW Equation (3.11)")  (statement := /--  Let $k=1,\ldots,5$. Assume there exist a positive integer $n$, real numbers $a_{\ell} \ge 0$ for every $\ell \in \{1, 2, \ldots, n \}$.  Let $b' > b \geq 2k$. Then $B_k \leq \tilde B_k$ where  $$ \tilde B_k := b^{k} \sum_{\ell=1}^n a_{\ell} \exp\left(-\frac{\ell b}{\ell+1}\right) + \varepsilon(b) (b')^k. $$  . -/)  (proof := /-- Observe that since $x\ge e^b > e^{2k} \ge e^{\frac{k(\ell+1)}{\ell}}$, then each $a_\ell (\log x)^k x^{-\frac{\ell}{\ell + 1}}$ decreases with $x$.  The claim follows since $\varepsilon(b) (\log x)^k$ increases with $x$. -/)  (latexEnv := "sublemma")  (discussion := 1253)]theorem bklnw_eq_3_11 (k n : ℕ) (hk : 1 ≤ k) (a : ℕ → ℝ) (ε : ℝ → ℝ) (b b' : ℝ)  (ha : ∀ ℓ ∈ Finset.Icc 1 n, 0 ≤ a ℓ)  (hε : 0 ≤ ε b)  (hbb : b < b') (hbk : b ≥ 2 * k) :  B k n a ε b b' ≤ Btilde k n a ε b b' := by  unfold B Btilde  haveI h_nonempty : Nonempty (Set.Icc (exp b) (exp b')) := by    use exp b    simp only [Set.mem_Icc, le_refl, true_and]    exact exp_le_exp.mpr hbb.le  have h_sum_le : ∀ x ∈ Set.Icc (exp b) (exp b'),      (∑ ℓ ∈ Finset.Icc 1 n, a ℓ * (log x)^k * x ^ (-(ℓ:ℝ) / (ℓ + 1)))      ≤ b ^ k * (∑ ℓ ∈ Finset.Icc 1 n, a ℓ * exp (- (ℓ:ℝ) * b / (ℓ + 1))) := by    intro x hx    have hx_pos : 0 < x := (exp_pos b).trans_le hx.1    have hx_log : b ≤ log x := (log_exp b).symm ▸ log_le_log (exp_pos b) hx.1    calc      (∑ ℓ ∈ Finset.Icc 1 n, a ℓ * (log x)^k * x ^ (-(ℓ:ℝ) / (ℓ + 1)))      _ = ∑ ℓ ∈ Finset.Icc 1 n, a ℓ * ((log x)^k * x ^ (-(ℓ:ℝ) / (ℓ + 1))) := by        apply Finset.sum_congr rfl; intro _ _; ring      _ ≤ ∑ ℓ ∈ Finset.Icc 1 n, a ℓ * (b ^ k * exp (- (ℓ:ℝ) * b / (ℓ + 1))) := by        apply Finset.sum_le_sum; intro ℓ hℓ        exact mul_le_mul_of_nonneg_left (bklnw_eq_3_11_term_le k hk ℓ (Finset.mem_Icc.mp hℓ).1 b hbk x hx_pos hx_log) (ha ℓ hℓ)      _ = b ^ k * (∑ ℓ ∈ Finset.Icc 1 n, a ℓ * exp (- (ℓ:ℝ) * b / (ℓ + 1))) := by        rw [Finset.mul_sum]; apply Finset.sum_congr rfl; intro _ _; ring  have h_eps_le : ∀ x ∈ Set.Icc (exp b) (exp b'),      ε b * (log x) ^ k ≤ ε b * b' ^ k := by    intro x hx    have hx_pos : 0 < x := (exp_pos b).trans_le hx.1    have h_log_ge : b ≤ log x := (log_exp b).symm ▸ log_le_log (exp_pos b) hx.1    have hb_nonneg : 0 ≤ b := by linarith [hbk, show 0 ≤ (k : ℝ) from Nat.cast_nonneg k]    have h_log_le : log x ≤ b' := (log_exp b').symm ▸ log_le_log hx_pos hx.2    exact mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (by linarith) h_log_le k) hε  refine ciSup_le ?_  · rintro ⟨x, hx⟩    exact add_le_add (h_sum_le x hx) (h_eps_le x hx)