Lcm.prod_p_ge

@[blueprint  "lem:pi-product"  (title := "Bounds for the \\(p_i\\)-product")  (statement := /--  With \(p_i\) as in Lemma~\ref{lem:choose-pi}, we have for large \(n\)  \begin{equation}\label{eq:pi-lower}    \prod_{i=1}^3 \Bigl(1 + \frac{1}{p_i(p_i+1)}\Bigr)    \ge    \prod_{i=1}^3    \Bigl(      1 + \frac{1}{\bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^{2i} (n + \sqrt{n})}    \Bigr).  \end{equation}  -/)  (proof := /--  By Lemma~\ref{lem:choose-pi}, \(p_i \le \sqrt{n} (1+1/\log^3\sqrt{n})^i\).  Hence  \[    p_i^2 \le n\bigl(1 + \tfrac{1}{\log^3 \sqrt{n}}\bigr)^{2i}  \quad\text{and}\quad    p_i+1 \le p_i(1 + 1/\sqrt{n}) \le (1+1/\sqrt{n}) p_i.  \]  From these one gets  \[    p_i(p_i+1) \le \bigl(1 + \tfrac{1}{\log^3 \sqrt{n}}\bigr)^{2i} (n + \sqrt{n}),  \]  and hence  \[    \frac{1}{p_i(p_i+1)} \ge    \frac{1}{\bigl(1 + \tfrac{1}{\log^3 \sqrt{n}}\bigr)^{2i} (n + \sqrt{n})}.  \]  Taking \(1+\cdot\) and multiplying over \(i=1,2,3\) gives \eqref{eq:pi-lower}.  -/)  (latexEnv := "lemma")]theorem prod_p_ge {n : ℕ} (hn : n ≥ X₀ ^ 2) :    ∏ i, (1 + (1 : ℝ) /        ((exists_p_primes hn).choose i * ((exists_p_primes hn).choose i + 1))) ≥      ∏ i : Fin 3,        (1 + 1 / ((1 + 1 / (log √(n : ℝ)) ^ 3) ^ (2 * (i : ℕ) + 2 : ℝ) * (n + √n))) := by  refine Finset.prod_le_prod (fun i _ => by positivity [hlog hn]) fun i _ => ?_  set p := (exists_p_primes hn).choose  have h₀ (i) : √n < p i := by    have : p 0 ≤ p i := by      apply (exists_p_primes hn).choose_spec.2.1.monotone      simp    grw [← this]    exact (exists_p_primes hn).choose_spec.2.2.2  gcongr 1 + 1 / ?_  · have := ((exists_p_primes hn).choose_spec.1 i).pos    positivity  have : p i ≤ √n * (1 + 1 / log √n ^ 3) ^ (i + 1 : ℝ) :=    (exists_p_primes hn).choose_spec.2.2.1 i  have h₁ : p i ^ 2 ≤ n * (1 + 1 / log √n ^ 3) ^ (2 * i + 2 : ℝ) := by    grw [this, mul_pow, sq_sqrt (by simp)]    norm_cast    rw [← pow_mul]    grind  have h₂ : p i + 1 ≤ p i * (1 / n * (n + √n)) := by    field_simp [this]    linear_combination √n * h₀ i - sq_sqrt (cast_nonneg n)  grw [h₂, ← mul_assoc, ← sq, h₁]  field_simp  rfl