Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.theorem_6_1

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3075 to 3148

Source documentation

Now we can start estimating $E_\pi$ . We make the following running hypotheses. Let $x_0 > 0$ be chosen such that $\pi(x_0)$ and $\theta(x_0)$ are computable, and let $x_1 \geq \max(x_0, 14)$ . Let $\{b_i\}_{i=1}^N$ be a finite partition of $[\log x_0, \log x_1]$ , with $b_1 = \log x_0$ and $b_N = \log x_1$ , and suppose that $\varepsilon_{\theta,\mathrm{num}}$ gives numerical bounds for $x = \exp(b_i)$ , for each $i=1,\dots,N$ .

Exact Lean statement

@[blueprint
  "fks2-theorem-6-1"
  (title := "FKS2 Theorem 6, substep 1")
  (statement := /-- With the above hypotheses, for all $x \geq x_1$ we have
  $$ E_\pi(x) \leq \varepsilon_{\theta,num}(x_1) + \frac{\log x}{x} \frac{x_0}{\log x_0} (E_\pi(x_0) + E_\theta(x_0))$$
  $$ + \frac{\log x}{x} \sum_{i=1}^{N-1} \varepsilon_{\theta,num}(e^{b_i}) \left( \Li(e^{b_{i+1}}) - \Li(e^{b_i}) + \frac{e^{b_i}}{b_i} - \frac{e^{b_{i+1}}}{b_{i+1}} \right) $$
  $$ + \varepsilon_{\theta,num}(x_1) \frac{\log x}{x} \int_{x_1}^{x} \frac{1}{(\log t)^2} \, dt. $$ -/)
  (proof := /-- This is obtained by combining Sublemma \ref{fks2-eq-30} with the admissibility of $\varepsilon_{\theta,num}$ and Lemma \ref{fks2-lemma-19}.
  -/)
  (latexEnv := "sublemma")
  (discussion := 715)]
theorem theorem_6_1 {x₀ x₁ : ℝ} (h : x₁ ≥ max x₀ 14)
  {N : ℕ} (b : Fin (N + 1) → ℝ) (hmono : Monotone b)
  (h_b_start : b 0 = log x₀)
  (h_b_end : b (Fin.last N) = log x₁)
  (εθ_num : ℝ → ℝ)
  (h_εθ_num : ∀ i : Fin (N+1), Eθ.numericalBound (exp (b i)) εθ_num) (x : ℝ) (hx : x ≥ x₁) (hx₀ : x₀ ≥ 2) :
  Eπ x ≤ εθ_num x₁ + (log x / x) * (x₀ / log x₀) * (Eπ x₀ + Eθ x₀) +
    (log x / x) * ∑ i ∈ Finset.Iio (Fin.last N),
      εθ_num (exp (b i)) *
      (Li (exp (b (i + 1))) - Li (exp (b i)) +
      exp (b i) / b i - exp (b (i + 1)) / b (i + 1)) +
    εθ_num x₁ * (log x / x) * ∫ t in x₁..x, 1 / (log t) ^ 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "fks2-theorem-6-1"  (title := "FKS2 Theorem 6, substep 1")  (statement := /-- With the above hypotheses, for all $x \geq x_1$ we have  $$ E_\pi(x) \leq \varepsilon_{\theta,num}(x_1) + \frac{\log x}{x} \frac{x_0}{\log x_0} (E_\pi(x_0) + E_\theta(x_0))$$  $$ + \frac{\log x}{x} \sum_{i=1}^{N-1} \varepsilon_{\theta,num}(e^{b_i}) \left( \Li(e^{b_{i+1}}) - \Li(e^{b_i}) + \frac{e^{b_i}}{b_i} - \frac{e^{b_{i+1}}}{b_{i+1}} \right) $$  $$ + \varepsilon_{\theta,num}(x_1) \frac{\log x}{x} \int_{x_1}^{x} \frac{1}{(\log t)^2} \, dt. $$ -/)  (proof := /-- This is obtained by combining Sublemma \ref{fks2-eq-30} with the admissibility of $\varepsilon_{\theta,num}$ and Lemma \ref{fks2-lemma-19}.  -/)  (latexEnv := "sublemma")  (discussion := 715)]theorem theorem_6_1 {x₀ x₁ : ℝ} (h : x₁ ≥ max x₀ 14)  {N : ℕ} (b : Fin (N + 1) → ℝ) (hmono : Monotone b)  (h_b_start : b 0 = log x₀)  (h_b_end : b (Fin.last N) = log x₁)  (εθ_num : ℝ → ℝ)  (h_εθ_num : ∀ i : Fin (N+1), Eθ.numericalBound (exp (b i)) εθ_num) (x : ℝ) (hx : x ≥ x₁) (hx₀ : x₀ ≥ 2) :  Eπ x ≤ εθ_num x₁ + (log x / x) * (x₀ / log x₀) * (Eπ x₀ + Eθ x₀) +    (log x / x) * ∑ i ∈ Finset.Iio (Fin.last N),      εθ_num (exp (b i)) *      (Li (exp (b (i + 1))) - Li (exp (b i)) +      exp (b i) / b i - exp (b (i + 1)) / b (i + 1)) +    εθ_num x₁ * (log x / x) * ∫ t in x₁..x, 1 / (log t) ^ 2 := by  have hx₀_le_x₁ : x₀ ≤ x₁ := le_trans (le_max_left _ _) h  have hx₀_le_x : x₀ ≤ x := le_trans hx₀_le_x₁ hx  have h30 := eq_30 hx₀_le_x hx₀  have hEθ_x_le : Eθ x ≤ εθ_num x₁ := by    have := h_εθ_num (Fin.last N)    rw [h_b_end, exp_log (by linarith [h])] at this    exact this x hx  have hδ_le : δ x₀ ≤ Eπ x₀ + Eθ x₀ := by    rw [δ, Eπ, Eθ]    refine (abs_sub_le _ 0 _).trans ?_    have hx₀_pos : 0 < x₀ := by positivity    have hlogx₀_pos : 0 < log x₀ := Real.log_pos (by linarith)    simp [abs_div, abs_of_pos hx₀_pos, abs_of_pos (by positivity : 0 < x₀ / log x₀)]  have hx₁_ge2 : x₁ ≥ 2 := by linarith [h]  have hsplit := intervalIntegral.integral_add_adjacent_intervals    (Eθ_integrable hx₀ hx₀_le_x₁) (Eθ_integrable hx₁_ge2 hx)  have hlogx_x_nonneg : 0 ≤ log x / x :=    div_nonneg (Real.log_nonneg (by linarith [hx, h])) (by linarith [hx, h])  have h_coeff_nonneg : 0 ≤ (log x / x) * (x₀ / log x₀) := by    apply mul_nonneg hlogx_x_nonneg    have : 0 < log x₀ := Real.log_pos (by linarith)    exact div_nonneg (by linarith) this.le  calc    Eπ x ≤        Eθ x        + (log x / x) * (x₀ / log x₀) * δ x₀        + (log x / x) * ∫ t in x₀..x, Eθ t / log t ^ 2 :=      h30    _ ≤ εθ_num x₁        + (log x / x) * (x₀ / log x₀) * (Eπ x₀ + Eθ x₀)        + (log x / x) * ∫ t in x₀..x, Eθ t / log t ^ 2 := by      gcongr    _ ≤ εθ_num x₁        + (log x / x) * (x₀ / log x₀) * (Eπ x₀ + Eθ x₀)        + (log x / x) *          ((∫ t in x₀..x₁, Eθ t / log t ^ 2)          + ∫ t in x₁..x, Eθ t / log t ^ 2) := by      rw [hsplit]    _ ≤ εθ_num x₁ + (log x / x) * (x₀ / log x₀) * (Eπ x₀ + Eθ x₀) +      (log x / x) * ∑ i ∈ Finset.Iio (Fin.last N),        εθ_num (exp (b i)) *          (Li (exp (b (i + 1))) - Li (exp (b i)) +          exp (b i) / b i - exp (b (i + 1)) / b (i + 1)) +      εθ_num x₁ * (log x / x) * ∫ t in x₁..x, 1 / (log t) ^ 2 := by      have h_bound_x1_x : ∫ t in x₁..x, Eθ t / log t ^ 2 ≤          εθ_num x₁ * ∫ t in x₁..x, 1 / (log t) ^ 2 := by        have := h_εθ_num (Fin.last N)        rw [h_b_end, exp_log (by linarith [h])] at this        exact Eθ_bound_integral_last hx₁_ge2 hx εθ_num this      have h_bound_x0_x1 := bound_x0_x1 hx₀ hx₀_le_x₁ b hmono h_b_start h_b_end εθ_num h_εθ_num      nlinarith [h_bound_x0_x1, h_bound_x1_x, hlogx_x_nonneg]