norm_zetaAbelContinuationFormula_le

theorem norm_zetaAbelContinuationFormula_le (s : ℂ) (hs : s ∈ zetaAbelContinuationDomain) :    ‖zetaAbelContinuationFormula s‖ ≤ 1 + ‖1 / (s - 1)‖ + ‖s‖ / s.re := by  set g : ℝ → ℝ := fun u => u ^ (-s.re - 1)  let μ := (volume : Measure ℝ).restrict (Ioi (1 : ℝ))  have hs_re := zetaAbelContinuationDomain_re_pos hs  have hint :      ‖s‖ * ‖∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u‖ ≤ ‖s‖ / s.re :=    mul_le_mul_of_nonneg_left      ((MeasureTheory.norm_integral_le_of_norm_le (μ := μ)        (f := fun u => zetaAbelFractKernel s u) (g := g)        (by          simpa [μ, g, IntegrableOn] using            (integrableOn_Ioi_rpow_of_lt (by linarith) one_pos))        (by          refine (ae_restrict_iff' measurableSet_Ioi).2 (MeasureTheory.ae_of_all _ ?_)          intro u hu          simpa [g] using norm_zetaAbelFractKernel_le u (le_of_lt hu) s)).trans        (by simpa [μ, g, one_div] using          (le_of_eq (by simp [integral_Ioi_rpow_neg_re_sub_one (s := s) hs_re]))))      (norm_nonneg s)  have hsplit :      ‖zetaAbelContinuationFormula s‖ ≤        1 + ‖(s - 1)⁻¹‖ + ‖s‖ * ‖∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u‖ := by    simp only [zetaAbelContinuationFormula, one_div]    calc      ‖1 + (s - 1)⁻¹ - s * ∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u‖          ≤ ‖1 + (s - 1)⁻¹‖ + ‖-s * ∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u‖ := by            simpa [sub_eq_add_neg] using              norm_add_le (1 + (s - 1)⁻¹) (-s * ∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u)      _ ≤ 1 + ‖(s - 1)⁻¹‖ + ‖s‖ * ‖∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u‖ := by        gcongr        · simpa [norm_one] using norm_add_le (1 : ℂ) ((s - 1)⁻¹)        · exact (norm_mul_le (-s) (∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u)).trans_eq            (by rw [norm_neg])  calc    ‖zetaAbelContinuationFormula s‖        ≤ 1 + ‖(s - 1)⁻¹‖ + ‖s‖ * ‖∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u‖ := hsplit    _ ≤ 1 + ‖(s - 1)⁻¹‖ + ‖s‖ / s.re := add_le_add_right hint _    _ ≤ 1 + ‖1 / (s - 1)‖ + ‖s‖ / s.re := by simp [one_div]