Lcm.prod_q_ge

@[blueprint  "lem:qi-product"  (title := "Bounds for the \\(q_i\\)-product")  (statement := /--  With \(p_i,q_i\) as in Lemmas~\ref{lem:choose-pi} and \ref{lem:choose-qi}, we have  \begin{equation}\label{eq:qi-upper}    \prod_{i=1}^3 \Bigl(1 + \frac{1}{q_i}\Bigr)    \le    \prod_{i=1}^3 \Bigl(1 + \frac{\bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^i}{n} \Bigr).  \end{equation}  -/)  (proof := /--  By Lemma~\ref{lem:choose-qi}, each \(q_i\) is at least  \[    n\Bigl(1 + \frac{1}{\log^3 \sqrt{n}}\Bigr)^{-j}  \]  for suitable indices \(j\), so \(1/q_i\) is bounded above by  \[    \frac{\bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^i}{n}  \]  after reindexing. Multiplying the three inequalities gives \eqref{eq:qi-upper}.  -/)  (proofUses := ["lem:choose-qi"])  (latexEnv := "lemma")]theorem prod_q_ge {n : ℕ} (hn : n ≥ X₀ ^ 2) :    ∏ i, (1 + (1 : ℝ) / (exists_q_primes hn).choose i) ≤      ∏ i : Fin 3, (1 + (1 + 1 / (log √(n : ℝ)) ^ 3) ^ ((i : ℕ) + 1 : ℝ) / n) := by  rw [show ∏ i : Fin 3, (1 + (1 + 1 / (log √(n : ℝ)) ^ 3) ^ ((i : ℕ) + 1 : ℝ) / n) =      ∏ i : Fin 3, (1 + (1 + 1 / (log √(n : ℝ)) ^ 3) ^ ((3 : ℝ) - (i : ℕ)) / n) by    simp only [Fin.prod_univ_three, Fin.val_zero, Fin.val_one, Fin.val_two]; ring_nf]  apply Finset.prod_le_prod (fun _ _ ↦ by positivity)  intro i _  suffices h : (1 : ℝ) / (exists_q_primes hn).choose i ≤      (1 + 1 / (log √(n : ℝ)) ^ 3) ^ ((3 : ℝ) - (i : ℕ)) / n from (by linarith)  have := (exists_q_primes hn).choose_spec.2.2.1 i  rw [show (1 + 1 / (log √(n : ℝ)) ^ 3) ^ ((3 : ℝ) - (i : ℕ)) / n =      1 / (n / (1 + 1 / (log √(n : ℝ)) ^ 3) ^ ((3 : ℝ) - (i : ℕ)) ) by field_simp]  have f0 : (0 : ℝ) < (log √(n : ℝ)) ^ 3 := by positivity [hlog hn]  apply one_div_le_one_div_of_le  · positivity  · convert! this using 1    field_simp    rw [← rpow_add (hε_pos hn)]    simp