R_locally_bounded

lemma R_locally_bounded (K : ℝ) (hK : 0 ≤ K) : ∃ C, ∀ y ∈ Set.Icc 0 K, |R y| ≤ C := by  have hR_bounded : BddAbove (Set.image (fun y => |R y|) (Set.Icc 0 K)) := by    have hR_bounded : ∀ y ∈ Set.Icc 0 K, |R y| ≤ ∑ p ∈ Iic ⌊K⌋₊, log p + K := by      intro y hy      simp only [R, Psi, Chebyshev.psi_eq_sum_Icc]      refine abs_sub_le_iff.mpr ⟨?_, ?_⟩      · refine le_trans (sub_le_self _ hy.1) ?_        refine le_trans (Finset.sum_le_sum_of_subset_of_nonneg (Finset.Iic_subset_Iic.mpr <| Nat.floor_mono hy.2) fun ?_ ?_ ?_ => ?_) ?_        · exact vonMangoldt_nonneg        · refine le_add_of_le_of_nonneg (Finset.sum_le_sum fun i hi => ?_) hK          exact vonMangoldt_le_log      · refine le_trans ?_ (le_add_of_nonneg_left ?_)        · exact le_trans (sub_le_self _ <| Finset.sum_nonneg fun _ _ => by exact_mod_cast ArithmeticFunction.vonMangoldt_nonneg) hy.2        · exact Finset.sum_nonneg fun _ _ => Real.log_natCast_nonneg _    exact ⟨_, Set.forall_mem_image.2 hR_bounded⟩  exact ⟨hR_bounded.choose, fun y hy => hR_bounded.choose_spec <| Set.mem_image_of_mem _ hy⟩