Source indexedtheorem · leanprover/lean4:v4.32.0

Lcm.pq_ratio_ge

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:1332 to 1393

Mathematical statement

Exact Lean statement

@[blueprint
  "lem:pq-ratio"
  (title := "Lower bound for the product ratio \\(p_i/q_i\\)")
  (statement := /--
  With \(p_i,q_i\) as in Lemmas~\ref{lem:choose-pi} and \ref{lem:choose-qi}, we have
  \begin{equation}\label{eq:pq-ratio}
    1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}
    \ge
    1 - \frac{4 \bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^{12}}{n^{3/2}}.
  \end{equation}
  -/)
  (proof := /--
  We have \(p_i \le \sqrt{n} (1+1/\log^3 \sqrt{n})^i\), so
  \[
    p_1 p_2 p_3 \le n^{3/2} \bigl(1 + \tfrac{1}{\log^3 \sqrt{n}}\bigr)^{6}.
  \]
  Similarly, \(q_i \ge n(1+1/\log^3 \sqrt{n})^{-i}\), so
  \[
    q_1 q_2 q_3 \ge n^3 \bigl(1 + \tfrac{1}{\log^3 \sqrt{n}}\bigr)^{-6}.
  \]
  Combining,
  \[
    \frac{p_1 p_2 p_3}{q_1 q_2 q_3} \le
    \frac{n^{3/2} \bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^{6}}{n^3
    \bigl(1 + \frac{1}{\log^3\sqrt{n}}\bigr)^{-6}}
    = \frac{\bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^{12}}{n^{3/2}}.
  \]
  This implies \eqref{eq:pq-ratio}.
  -/)
  (latexEnv := "lemma")
  (discussion := 534)]
theorem pq_ratio_ge {n : ℕ} (hn : n ≥ X₀ ^ 2) :
    1 - ((4 : ℝ) * ∏ i, ((exists_p_primes hn).choose i : ℝ))
    / ∏ i, ((exists_q_primes hn).choose i : ℝ) ≥
    1 - 4 * (1 + 1 / (log √(n : ℝ)) ^ 3) ^ 12 / n ^ (3 / 2 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "lem:pq-ratio"  (title := "Lower bound for the product ratio \\(p_i/q_i\\)")  (statement := /--  With \(p_i,q_i\) as in Lemmas~\ref{lem:choose-pi} and \ref{lem:choose-qi}, we have  \begin{equation}\label{eq:pq-ratio}    1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}    \ge    1 - \frac{4 \bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^{12}}{n^{3/2}}.  \end{equation}  -/)  (proof := /--  We have \(p_i \le \sqrt{n} (1+1/\log^3 \sqrt{n})^i\), so  \[    p_1 p_2 p_3 \le n^{3/2} \bigl(1 + \tfrac{1}{\log^3 \sqrt{n}}\bigr)^{6}.  \]  Similarly, \(q_i \ge n(1+1/\log^3 \sqrt{n})^{-i}\), so  \[    q_1 q_2 q_3 \ge n^3 \bigl(1 + \tfrac{1}{\log^3 \sqrt{n}}\bigr)^{-6}.  \]  Combining,  \[    \frac{p_1 p_2 p_3}{q_1 q_2 q_3} \le    \frac{n^{3/2} \bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^{6}}{n^3    \bigl(1 + \frac{1}{\log^3\sqrt{n}}\bigr)^{-6}}    = \frac{\bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^{12}}{n^{3/2}}.  \]  This implies \eqref{eq:pq-ratio}.  -/)  (latexEnv := "lemma")  (discussion := 534)]theorem pq_ratio_ge {n : ℕ} (hn : n ≥ X₀ ^ 2) :    1 - ((4 : ℝ) * ∏ i, ((exists_p_primes hn).choose i : ℝ))    / ∏ i, ((exists_q_primes hn).choose i : ℝ) ≥    1 - 4 * (1 + 1 / (log √(n : ℝ)) ^ 3) ^ 12 / n ^ (3 / 2 : ℝ) := by  have l1 : ((1 + 1 / Real.log √n ^ 3) ^ 12 / n ^ (3 / 2 : ℝ)) =    (n ^ (3 / 2 : ℝ) * (1 + 1 / Real.log √n ^ 3) ^ 6) /    (n ^ (3 : ℝ) * (1 + 1 / Real.log √n ^ 3) ^ (- 6 : ℝ)) := by    rw [rpow_neg (hε_pos hn).le, ← div_eq_mul_inv, div_div_eq_mul_div, mul_assoc,      mul_comm, ← rpow_natCast, ← rpow_natCast (n := 6), ← rpow_add (hε_pos hn),      ← div_div_eq_mul_div]    · congr      · grind      · rw [← rpow_sub (by norm_cast; linarith)]; grind  have l2 : n ^ (3 / 2 : ℝ) * (1 + 1 / Real.log √n ^ 3) ^ 6 = ∏ i : Fin 3,    √n * (1 + 1 / Real.log √n ^ 3) ^ ((i : ℝ) + 1) := by    rw [← Finset.pow_card_mul_prod, Fin.prod_univ_three, ← rpow_add (hε_pos hn),      ← rpow_add (hε_pos hn), rpow_div_two_eq_sqrt _ (by linarith)]    norm_num  have l3 : n ^ (3 : ℝ) * (1 + 1 / Real.log √n ^ 3) ^ (- 6 : ℝ) =    ∏ i : Fin 3, n * (1 + 1 / Real.log √n ^ 3) ^ (-((3 : ℝ) - i.1))  := by    rw [← Finset.pow_card_mul_prod, Fin.prod_univ_three, ← rpow_add (hε_pos hn),      ← rpow_add (hε_pos hn)]    norm_num  rw [← mul_div_assoc', ← mul_div_assoc', l1, l2, l3]  gcongr  · have := hε_pos hn    exact Finset.prod_nonneg fun _ _ => by positivity  · exact Finset.prod_pos fun _ _ => by positivity [hε_pos hn]  · exact (exists_p_primes hn).choose_spec.2.2.1 _  · exact fun _ _ => by positivity [hε_pos hn]  · exact (exists_q_primes hn).choose_spec.2.2.1 _