Chebyshev.U_bound

@[blueprint  "U-bounds"  (title := "Bounds for $U$")  (statement := /-- For $x \geq 30$, we have $|U(x) - ax| \leq 5\log x - 5$. -/)  (proof := /-- Use Lemma \ref{cheby-T-upper}, Lemma \ref{cheby-T-lower}, the definition of $a$, and the triangle inequality, also using that $\log(2)+\log(3)+\log(5)+\log(30) \geq 6$. -/)  (latexEnv := "lemma")  (discussion := 840)]theorem U_bound (x : ℝ) (hx : 30 ≤ x) : |U x - a * x| ≤ 5 * log x - 5 := by  have hxpos : 0 < x := lt_of_lt_of_le (by norm_num) hx  rw [U_bound.lemma_3, U_bound.lemma_4 x hxpos]  ring_nf  have hlin : ν.sum (fun m w ↦ x * w * (↑m)⁻¹) = 0 :=    by simpa [div_eq_mul_inv, mul_assoc, mul_left_comm] using U_bound.lemma_5 x  rw [hlin]; ring_nf; rw [U_bound.lemma_6]  grw [abs_add_le, Finsupp.abs_sum_le]  norm_num  have hsupp_eq : ν.support = {1, 2, 3, 5, 30} := ν_support  have hmem_of_supp : ∀ i ∈ ν.support, 0 < i ∧ i ≤ 30 := fun i hi ↦ by    have : i ∈ ({1, 2, 3, 5, 30} : Finset ℕ) := hsupp_eq ▸ hi    simp only [mem_insert, mem_singleton] at this    constructor <;> omega  have h : ν.sum |fun m w ↦ w * e (x * (↑m)⁻¹)| ≤ ν.sum (fun m w ↦ |w| * log (x * (↑m)⁻¹)) := by    apply Finsupp.sum_le_sum    intro i hi    simp only [Pi.abs_apply, abs_mul]    obtain ⟨hi_pos, hi_le⟩ := hmem_of_supp i hi    have hxi : 1 ≤ x * (↑i)⁻¹ := by      rw [le_mul_inv_iff₀ (by exact_mod_cast hi_pos)]      linarith [show (i : ℝ) ≤ 30 from by exact_mod_cast hi_le]    gcongr; exact U_bound.lemma_2 _ hxi  grw [h]  have hlog_split : ν.sum (fun m w ↦ |w| * log (x * (m : ℝ)⁻¹)) =      log x * ν.sum (fun m w ↦ |w|) - ν.sum (fun m w ↦ |w| * log (↑m : ℝ)) := by    simp only [Finsupp.sum]    conv_rhs => rw [Finset.mul_sum, ← sum_sub_distrib]    apply Finset.sum_congr rfl    intro m hm    have hm_pos : (0 : ℝ) < m := by exact_mod_cast (hmem_of_supp m hm).1    rw [← div_eq_mul_inv, Real.log_div (ne_of_gt hxpos) (ne_of_gt hm_pos)]; ring  rw [hlog_split]  -- Once the support of `ν` is known explicitly, both `habs` and `hsum_eq`  -- reduce to concrete arithmetic over a five-element finset.  have expand_sum : ∀ f : ℕ → ℝ → ℝ, (∀ n, f n 0 = 0) →      ν.sum f = f 1 1 + f 2 (-1) + f 3 (-1) + f 5 (-1) + f 30 1 := by    intro f hf    rw [Finsupp.sum_of_support_subset _ hsupp_eq.le _ (by intros; simp [hf])]    simp only [sum_insert (by decide : (1:ℕ) ∉ ({2,3,5,30} : Finset ℕ)),               sum_insert (by decide : (2:ℕ) ∉ ({3,5,30} : Finset ℕ)),               sum_insert (by decide : (3:ℕ) ∉ ({5,30} : Finset ℕ)),               sum_insert (by decide : (5:ℕ) ∉ ({30} : Finset ℕ)),               sum_singleton, ν, Finsupp.sub_apply, Finsupp.add_apply, Finsupp.single_apply]    norm_num    ring  have habs : ν.sum (fun m w ↦ |w|) = 5 := by    rw [expand_sum _ (by intros; simp)]; norm_num  have hgeq6 : ν.sum (fun m w ↦ |w| * log m) ≥ 6 := by    have hsum_eq : ν.sum (fun m w ↦ |w| * log (m : ℝ)) = log 2 + log 3 + log 5 + log 30 := by      rw [expand_sum _ (by intros; simp)]      simp [log_one]    linarith [log_2_gt, log_3_gt, log_5_gt, log_30_gt]  grw [hgeq6]; rw [habs]; linarith