BKLNW.prop_3

@[blueprint  "bklnw-prop-3"  (title := "BKLNW Proposition 3")  (statement := /--  Let $x_0 \geq 2^9$. Let $\alpha > 0$ exist such that $\theta(x) \leq (1 + \alpha)x$ for $x > 0$. Then for $x \geq x_0$,\begin{equation}\sum_{k=3}^{\lfloor \frac{\log x}{\log 2} \rfloor} \theta(x^{1/k}) \leq \eta x^{1/3},\end{equation}where\begin{equation}\eta = \eta(x_0) = (1 + \alpha) \max\left(f(x_0), f(2^{\lfloor \frac{\log x_0}{\log 2} \rfloor + 1})\right)\end{equation}with\begin{equation}f(x) := \sum_{k=3}^{\lfloor \frac{\log x}{\log 2} \rfloor} x^{\frac{1}{k} - \frac{1}{3}}.\end{equation} -/)  (proof := /-- Combines previous sublemmas. -/)  (latexEnv := "proposition")  (discussion := 639)]theorem prop_3 (I : Inputs) {x₀ x : ℝ} (hx₀ : x₀ ≥ 2 ^ 9) (hx : x ≥ x₀) :    ∑ k ∈ Icc 3 ⌊(log x)/(log 2)⌋₊, θ (x^(1/(k:ℝ))) ≤      (1 + I.α) * max (f x₀) (f (2^(⌊(log x₀)/(log 2)⌋₊ + 1))) * x^(1/3:ℝ) := by  have h_sum_le : ∑ k ∈ Icc 3 ⌊(log x) / (log 2)⌋₊, θ (x^(1 / k : ℝ)) ≤      (1 + I.α) * f x * x^(1 / 3 : ℝ) := by    have h_sum_le' : ∑ k ∈ Icc 3 ⌊(log x) / (log 2)⌋₊, θ (x^(1 / k : ℝ)) ≤        ∑ k ∈ Icc 3 ⌊(log x) / (log 2)⌋₊, (1 + I.α) * x^(1 / k : ℝ) := sum_le_sum fun i hi ↦ by      have := I.hα (x ^ (1 / (i : ℝ))) (rpow_pos_of_pos (by grind) _)      norm_num [log_rpow (by positivity)] at *      exact this    convert h_sum_le' using 1    norm_num [f, mul_sum .., mul_assoc, mul_comm, mul_left_comm, sum_mul]    refine sum_bij (fun k hk ↦ k) ?_ ?_ ?_ ?_ <;> norm_num    intro a ha₁ ha₂; rw [← rpow_add (by grind)]; grind  apply le_trans h_sum_le ?_  gcongr  · exact rpow_nonneg (by grind) _  · have := I.hα 1    grind [show 0 ≤ θ 1 from sum_nonneg fun _ _ ↦ log_nonneg <| Nat.one_le_cast.2 <|      Nat.Prime.pos <| by grind only [= mem_filter]]  · exact prop_3_sub_8 x₀ hx₀ x hx