ZetaAppendix.lemma_IBP_bound_C1_monotone

theorem lemma_IBP_bound_C1_monotone {a b : ℝ} (hab : a < b) (g : ℝ → ℝ) (F : ℝ → ℂ)    (hg : ContDiffOn ℝ 1 g (Icc a b)) (hg_mono : MonotoneOn g (Icc a b))    (hF : ContDiffOn ℝ 1 F (Icc a b)) :    ‖(∫ t in Icc a b, (g t : ℂ) * deriv F t) - (g b * F b - g a * F a)‖ ≤    (⨆ t ∈ Icc a b, ‖F t‖) * (g b - g a) := by  have hbound := @lemma_IBP_bound_C1 a b hab g F hg hF  have hdiff : DifferentiableOn ℝ g (Icc a b) := hg.differentiableOn_one  have hderiv_nonneg : ∀ t ∈ Ioo a b, 0 ≤ deriv g t := by    intro t ht    have hlim : Tendsto (fun h ↦ (g (t + h) - g t) / h) (𝓝[Ioi 0] 0) (𝓝 (deriv g t)) := by      have hHasDeriv : HasDerivAt g (deriv g t) t :=        hdiff.differentiableAt (Icc_mem_nhds ht.1 ht.2) |>.hasDerivAt      simpa [div_eq_inv_mul] using hHasDeriv.tendsto_slope_zero_right    refine le_of_tendsto_of_tendsto tendsto_const_nhds hlim ?_    filter_upwards [Ioo_mem_nhdsGT (sub_pos.mpr ht.2)] with h hh    apply div_nonneg    · rw [sub_nonneg]      refine hg_mono (Ioo_subset_Icc_self ht) ?_ (by linarith [hh.1])      rw [Set.mem_Icc]      constructor <;> linarith [ht.1, ht.2, hh.1, hh.2]    · exact hh.1.le  have hint_deriv : ∫ t in Icc a b, deriv g t = g b - g a := by    rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hab.le]    apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le hab.le hg.continuousOn    · intro t ht      exact hdiff.differentiableAt (Icc_mem_nhds ht.1 ht.2) |>.hasDerivAt    · rw [intervalIntegrable_iff_integrableOn_Ioo_of_le hab.le]      have hcont_dw := hg.continuousOn_derivWithin (uniqueDiffOn_Icc hab) le_rfl      refine hcont_dw.integrableOn_Icc.mono_set Ioo_subset_Icc_self |>.congr_fun ?_ measurableSet_Ioo      intro x hx      rw [derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)]  have hint_abs : ∫ t in Icc a b, |deriv g t| = ∫ t in Icc a b, deriv g t := by    simp only [integral_Icc_eq_integral_Ioc, integral_Ioc_eq_integral_Ioo]    refine setIntegral_congr_fun measurableSet_Ioo fun x hx ↦ ?_    rw [abs_of_nonneg (hderiv_nonneg x hx)]  rw [hint_abs, hint_deriv] at hbound  exact hbound