bound_sum_log

lemma bound_sum_log {C : ℝ} (hf0 : f 0 = 0) (hf : chebyWith C f) {x : ℝ} (hx : 1 ≤ x) :    ∑' i, ‖f i‖ / i * (1 + (1 / (2 * π) * log (i / x)) ^ 2)⁻¹ ≤      C * (1 + ∫ t in Ioi 0, hh (1 / (2 * π)) t) := by   let ggg (i : ℕ) : ℝ := if i = 0 then 1 else gg x i   have l0 : x ≠ 0 := by linarith  have l1 i : 0 ≤ ggg i := by by_cases hi : i = 0 <;> simp only [gg, one_div, mul_inv_rev, hi,    ↓reduceIte, zero_le_one, ggg] ; positivity  have l2 : Antitone ggg := by    intro i j hij ; by_cases hi : i = 0 <;> by_cases hj : j = 0 <;> simp only [hj, ↓reduceIte, hi,      le_refl, ggg]    · exact gg_le_one _    · omega    · simp only [gg_of_hh l0]      gcongr      apply hh_antitone one_div_two_pi_mem_Ioo      · simp only [mem_Ioi] ; positivity      · simp only [mem_Ioi] ; positivity      · gcongr  have l3 : 0 ≤ C := by simpa [cumsum, hf0] using hf 1   have l4 : 0 ≤ ∫ (t : ℝ) in Ioi 0, hh (π⁻¹ * 2⁻¹) t :=    setIntegral_nonneg measurableSet_Ioi (fun x hx => hh_nonneg _ (LT.lt.le hx))   have l5 {n : ℕ} : AntitoneOn (fun t ↦ x⁻¹ * hh (1 / (2 * π)) (t / x)) (Ioc 0 n) := by    intro u ⟨hu1, _⟩ v ⟨hv1, _⟩ huv    simp only    apply mul_le_mul le_rfl ?_ (hh_nonneg _ (by positivity)) (by positivity)    apply hh_antitone one_div_two_pi_mem_Ioo (by simp only [mem_Ioi] ; positivity)      (by simp only [mem_Ioi] ; positivity)    apply (div_le_div_iff_of_pos_right (by positivity)).mpr huv   have l6 {n : ℕ} : IntegrableOn (fun t ↦ x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Icc 0 n) volume := by    apply IntegrableOn.mono_set      (hh_integrable (by positivity) (by positivity) (by positivity)) Icc_subset_Ici_self   apply Real.tsum_le_of_sum_range_le (fun n => by positivity) ; intro n  convert_to! ∑ i ∈ Finset.range n, ‖f i‖ * ggg i ≤ _  · congr ; ext i    by_cases hi : i = 0    · simp [hi, hf0]    · simp only [gg, hi, ↓reduceIte, ggg]      field_simp   apply cancel_main' (fun _ => norm_nonneg _) (by simp [hf0]) l1 hf l2 n |>.trans  gcongr ; simp only [cumsum, gg_of_hh l0, one_div, mul_inv_rev, ggg]   by_cases hn : n = 0  · simp only [hn, Finset.range_zero, Finset.sum_empty] ; positivity  replace hn : 0 < n := by omega  have : Finset.range n = {0} ∪ Finset.Ico 1 n := by    ext i ; simp ; by_cases hi : i = 0 <;> simp [hi, hn] ; omega  simp only [this, Finset.singleton_union, Finset.mem_Ico, nonpos_iff_eq_zero, one_ne_zero,    false_and, not_false_eq_true, Finset.sum_insert, ↓reduceIte, add_le_add_iff_left, ge_iff_le]  convert_to! ∑ x_1 ∈ Finset.Ico 1 n, x⁻¹ * hh (π⁻¹ * 2⁻¹) (↑x_1 / x) ≤ _  · apply Finset.sum_congr rfl (fun i hi => ?_)    simp at hi    have : i ≠ 0 := by omega    simp [this]  simp_rw [Finset.sum_Ico_eq_sum_range, add_comm 1]  have := @sum_le_integral 0 (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (n - 1)    (by simpa using l5) (by simpa using l6)  simp only [zero_add] at this  apply this.trans  rw [@intervalIntegral.integral_comp_div ℝ _ _ 0 ↑(n - 1) x (fun t => x⁻¹ * hh (π⁻¹ * 2⁻¹) (t)) l0]  simp only [zero_div, intervalIntegral.integral_const_mul, smul_eq_mul, ← mul_assoc,    mul_inv_cancel₀ l0, one_mul]  have : (0 : ℝ) ≤ ↑(n - 1) / x := by positivity  rw [intervalIntegral.intervalIntegral_eq_integral_uIoc]  simp only [this, ↓reduceIte, uIoc_of_le, smul_eq_mul, one_mul, ge_iff_le]  apply integral_mono_measure  · apply Measure.restrict_mono Ioc_subset_Ioi_self le_rfl  · apply eventually_of_mem (self_mem_ae_restrict measurableSet_Ioi)    intro x (hx : 0 < x)    apply hh_nonneg _ hx.le  · have := (@hh_integrable 1 (1 / (2 * π)) 1 (by positivity) (by positivity) (by positivity))    simpa using! this.mono_set Ioi_subset_Ici_self