bound_I2

lemma bound_I2 (x : ℝ) (ψ : W21) :    ‖∫ u in Set.Ici (-log x), 𝓕 (ψ : ℝ → ℂ) (u / (2 * π))‖ ≤ W21.norm ψ * (2 * π ^ 2) := by   have key a : ‖𝓕 (ψ : ℝ → ℂ) (a / (2 * π))‖ ≤ W21.norm ψ * (1 + (a / (2 * π)) ^ 2)⁻¹ :=    decay_bounds_key ψ _  have twopi : 0 ≤ 2 * π := by simp [pi_nonneg]  have l3 : Integrable (fun a ↦ (1 + (a / (2 * π)) ^ 2)⁻¹) :=    integrable_inv_one_add_sq.comp_div (by norm_num [pi_ne_zero])  have l2 : IntegrableOn (fun i ↦ W21.norm ψ * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-Real.log x)) := by    exact (l3.const_mul _).integrableOn  have l1 : IntegrableOn (fun i ↦ ‖𝓕 (ψ : ℝ → ℂ) (i / (2 * π))‖) (Ici (-Real.log x)) := by    refine ((l3.const_mul (W21.norm ψ)).mono' ?_ ?_).integrableOn    · apply Continuous.aestronglyMeasurable ; fun_prop    · simp only [norm_norm, key] ; simp  have l5 : 0 ≤ᵐ[volume] fun a ↦ (1 + (a / (2 * π)) ^ 2)⁻¹ := by    apply Eventually.of_forall ; intro x ; positivity  refine (norm_integral_le_integral_norm _).trans <| (setIntegral_mono l1 l2 key).trans ?_  rw [integral_const_mul] ; gcongr  · apply W21.norm_nonneg  refine (setIntegral_le_integral l3 l5).trans ?_  rw [Measure.integral_comp_div (fun x => (1 + x ^ 2)⁻¹) (2 * π)]  simp [abs_eq_self.mpr twopi] ; ring_nf ; rfl