Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.remark_7

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3714 to 3744

Source documentation

For $x_1 \leq x_2$ , we define $\epsilon_{\pi,num}(x_0,x_1,x_2) := \epsilon_{\theta,num}(x_1) (1 + \mu_{num}(x_0,x_1,x_2))$ . -/)] noncomputable def επ_num {N : ℕ} (b : Fin (N + 1) → ℝ) (εθ_num : ℝ → ℝ) (x₀ x₁ : ℝ) (x₂ : EReal) : ℝ := εθ_num x₁ * (1 + μ_num b εθ_num x₀ x₁ x₂)

noncomputable def default_b (x₀ x₁ : ℝ) : Fin 2 → ℝ := fun i ↦ if i = 0 then log x₀ else log x₁

/- [NOTE]: The original FKS2 paper states the derivative condition deriv (fun x ↦ (log x) / x * (Li x - x / log x - Li x₁ + x₁ / log x₁)) x₂ ≥ 0 as a hypothesis for this remark. However, Aristotle's proof shows it is not required.

Exact Lean statement

@[blueprint
  "fks2-remark-7"
  (title := "FKS2 Remark 7")
  (statement := /--
  If
  $$ \frac{d}{dx} \frac{\log x}{x}
    \left( \Li(x) - \frac{x}{\log x} - \Li(x_1) + \frac{x_1}{\log x_1} \right)|_{x_2} \geq 0 $$
  then $\mu_{num,1}(x_0,x_1,x_2) < \mu_{num,2}(x_0,x_1)$.
  -/)
  (proof := /-- This follows from the definitions of $\mu_{num,1}$ and $\mu_{num,2}$. -/)
  (latexEnv := "remark")
  (discussion := 673)]
theorem remark_7 {x₀ x₁ : ℝ} (x₂ : ℝ) (h : x₁ ≥ max x₀ 14)
    {N : ℕ} (b : Fin (N + 1) → ℝ) (εθ_num : ℝ → ℝ) (x : ℝ) (hx₁ : x₁ ≤ x) (hx₂ : x ≤ x₂) :
    μ_num_1 b εθ_num x₀ x₁ x₂ < μ_num_2 b εθ_num x₀ x₁

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "fks2-remark-7"  (title := "FKS2 Remark 7")  (statement := /--  If  $$ \frac{d}{dx} \frac{\log x}{x}    \left( \Li(x) - \frac{x}{\log x} - \Li(x_1) + \frac{x_1}{\log x_1} \right)|_{x_2} \geq 0 $$  then $\mu_{num,1}(x_0,x_1,x_2) < \mu_{num,2}(x_0,x_1)$.  -/)  (proof := /-- This follows from the definitions of $\mu_{num,1}$ and $\mu_{num,2}$. -/)  (latexEnv := "remark")  (discussion := 673)]theorem remark_7 {x₀ x₁ : ℝ} (x₂ : ℝ) (h : x₁ ≥ max x₀ 14)    {N : ℕ} (b : Fin (N + 1) → ℝ) (εθ_num : ℝ → ℝ) (x : ℝ) (hx₁ : x₁ ≤ x) (hx₂ : x ≤ x₂) :    μ_num_1 b εθ_num x₀ x₁ x₂ < μ_num_2 b εθ_num x₀ x₁ := by  simp only [μ_num_2, μ_num_1, sup_le_iff, add_lt_add_iff_left] at *  convert theorem_6_2 (by linarith : x₁ ≥ 14) x₂ (by linarith) using 1  · rw [intervalIntegral.integral_eq_sub_of_hasDerivAt]; rotate_right    · exact fun x ↦ Li x - x / log x    · ring_nf    · intro x hx      convert! HasDerivAt.sub (hasDerivAt_Li _) (HasDerivAt.div (hasDerivAt_id x)        (hasDerivAt_log _) _) using 1 <;>        ring_nf <;> norm_num [show x ≠ 0 by cases Set.mem_uIcc.mp hx <;> linarith,          show log x ≠ 0 by exact ne_of_gt <| log_pos <| by cases Set.mem_uIcc.mp hx <;> linarith]      · by_cases h : log x = 0 <;> simp [sq, h]      · cases Set.mem_uIcc.mp hx <;> linarith    · apply_rules [ContinuousOn.intervalIntegrable]      exact continuousOn_of_forall_continuousAt fun t ht ↦ ContinuousAt.div continuousAt_const        (ContinuousAt.pow (continuousAt_log (by cases Set.mem_uIcc.mp ht <;> linarith)) _)          (ne_of_gt (sq_pos_of_pos (log_pos (by cases Set.mem_uIcc.mp ht <;> linarith))))