ZetaAppendix.lemma_IBP_bound_C1

theorem lemma_IBP_bound_C1 {a b : ℝ} (hab : a < b) (g : ℝ → ℝ) (F : ℝ → ℂ)    (hg : ContDiffOn ℝ 1 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‖) * ∫ t in Icc a b, |deriv g t| := by  have hint_parts : ∫ t in Icc a b, (g t) * (deriv F t) =      (g b) * (F b) - (g a) * (F a) - ∫ t in Icc a b, (F t) * (deriv g t) := by    rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hab.le,      integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hab.le,        eq_sub_iff_add_eq, ← intervalIntegral.integral_add, intervalIntegral.integral_eq_sub_of_hasDeriv_right]    · simpa only [Set.uIcc_of_le hab.le] using! ContinuousOn.mul        (continuous_ofReal.comp_continuousOn hg.continuousOn) hF.continuousOn    · intro x hx      have hxa : x > a := by cases max_cases a b <;> cases min_cases a b <;> linarith [hx.1, hx.2]      have hxb : x < b := by cases max_cases a b <;> cases min_cases a b <;> linarith [hx.1, hx.2]      convert! HasDerivAt.hasDerivWithinAt <| HasDerivAt.mul        (HasDerivAt.ofReal_comp <| hg.differentiableOn_one |> DifferentiableOn.hasDerivAt <| Icc_mem_nhds hxa hxb)          (hF.differentiableOn_one |> DifferentiableOn.hasDerivAt <| Icc_mem_nhds hxa hxb)            using 1      ring    · rw [intervalIntegrable_iff_integrableOn_Ioo_of_le hab.le]      refine Integrable.add ?_ ?_      · have hintF : IntegrableOn (fun x ↦ deriv F x) (Ioo a b) := by          have hcont := hF.continuousOn_derivWithin          have hintF' : IntegrableOn (fun x ↦ derivWithin F (Icc a b) x) (Ioo a b) :=            (hcont (uniqueDiffOn_Icc hab) le_rfl |> ContinuousOn.integrableOn_Icc) |>              fun h ↦ h.mono_set Ioo_subset_Icc_self          refine hintF'.congr ?_          filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx using            by rw [derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)]        apply Integrable.mono' _ _ _        · exact fun x ↦ ‖deriv F x‖ * sSup (Set.image (fun x ↦ |g x|) (Icc a b))        · exact Integrable.mul_const hintF.norm _        · exact AEStronglyMeasurable.mul            (continuous_ofReal.comp_aestronglyMeasurable              (hg.continuousOn.aestronglyMeasurable measurableSet_Icc |>                fun h ↦ h.mono_set Ioo_subset_Icc_self))            hintF.aestronglyMeasurable        · filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx using by            simpa [mul_comm] using mul_le_mul_of_nonneg_left              (le_csSup (IsCompact.bddAbove (isCompact_Icc.image_of_continuousOn                (continuous_abs.comp_continuousOn hg.continuousOn)))                (Set.mem_image_of_mem _ <| Ioo_subset_Icc_self hx)) (norm_nonneg _)      · have hintg : IntegrableOn (fun x ↦ deriv g x) (Ioo a b) := by          have hcont := hg.continuousOn_derivWithin (uniqueDiffOn_Icc hab) le_rfl          have hintg' : IntegrableOn (fun x ↦ derivWithin g (Icc a b) x) (Ioo a b) :=            hcont.integrableOn_Icc.mono_set Ioo_subset_Icc_self          exact hintg'.congr_fun (fun x hx ↦            by simp only [derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)]) measurableSet_Ioo        have hintFg : IntegrableOn (fun x ↦ F x * deriv g x) (Ioo a b) := by          have hbdd : ∃ C, ∀ x ∈ Ioo a b, ‖F x‖ ≤ C :=            IsCompact.exists_bound_of_continuousOn isCompact_Icc hF.continuousOn |>              fun ⟨C, hC⟩ ↦ ⟨C, fun x hx ↦ hC x <| Ioo_subset_Icc_self hx⟩          apply Integrable.mono' _ _ _          · exact fun x ↦ hbdd.choose * ‖deriv g x‖          · exact Integrable.const_mul hintg.norm _          · exact AEStronglyMeasurable.mul              (hF.continuousOn.aestronglyMeasurable measurableSet_Icc |>                fun h ↦ h.mono_set Ioo_subset_Icc_self)              (continuous_ofReal.comp_aestronglyMeasurable hintg.aestronglyMeasurable)          · filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx using by              simpa using mul_le_mul_of_nonneg_right (hbdd.choose_spec x hx)                (norm_nonneg (deriv g x))        exact hintFg    · rw [intervalIntegrable_iff_integrableOn_Ioo_of_le hab.le]      have hintF : IntegrableOn (fun x ↦ deriv F x) (Ioo a b) := by        have hcont := hF.continuousOn_derivWithin        have hintF' : IntegrableOn (fun x ↦ derivWithin F (Icc a b) x) (Ioo a b) :=          (hcont (uniqueDiffOn_Icc hab) le_rfl |> ContinuousOn.integrableOn_Icc) |>            fun h ↦ h.mono_set Ioo_subset_Icc_self        refine hintF'.congr ?_        filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx using          by rw [derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)]      refine hintF.norm.const_mul ?_ |> fun h ↦ h.mono' ?_ ?_      · exact sSup (Set.image (fun x ↦ ‖g x‖) (Icc a b))      · exact AEStronglyMeasurable.mul          (continuous_ofReal.comp_aestronglyMeasurable            (hg.continuousOn.aestronglyMeasurable measurableSet_Icc |>              fun h ↦ h.mono_set Ioo_subset_Icc_self))          hintF.aestronglyMeasurable      · filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx using by          simpa [abs_mul] using mul_le_mul_of_nonneg_right            (le_csSup (IsCompact.bddAbove (isCompact_Icc.image_of_continuousOn hg.continuousOn.norm))              (Set.mem_image_of_mem _ <| Ioo_subset_Icc_self hx)) (norm_nonneg _)    · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hab.le]      have hintg : IntegrableOn (fun x ↦ deriv g x) (Ioc a b) := by        have hintg' : IntegrableOn (fun x ↦ deriv g x) (Ioo a b) := by          have hcont := hg.continuousOn_derivWithin (uniqueDiffOn_Icc hab) le_rfl          have hintg'' : IntegrableOn (fun x ↦ derivWithin g (Icc a b) x) (Ioo a b) :=            hcont.integrableOn_Icc.mono_set Ioo_subset_Icc_self          exact hintg''.congr_fun (fun x hx ↦            by simp only [derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)]) measurableSet_Ioo        rwa [IntegrableOn, Measure.restrict_congr_set Ioo_ae_eq_Ioc] at *      have hintFg : IntegrableOn (fun x ↦ F x * deriv g x) (Ioc a b) := by        have hbdd : ∃ C, ∀ x ∈ Ioc a b, ‖F x‖ ≤ C :=          IsCompact.exists_bound_of_continuousOn isCompact_Icc hF.continuousOn |>            fun ⟨C, hC⟩ ↦ ⟨C, fun x hx ↦ hC x <| Ioc_subset_Icc_self hx⟩        apply Integrable.mono' _ _ _        · exact fun x ↦ hbdd.choose * ‖deriv g x‖        · exact Integrable.const_mul hintg.norm _        · exact AEStronglyMeasurable.mul            (hF.continuousOn.aestronglyMeasurable measurableSet_Icc |>              fun h ↦ h.mono_set Ioc_subset_Icc_self)            (continuous_ofReal.comp_aestronglyMeasurable hintg.aestronglyMeasurable)        · filter_upwards [ae_restrict_mem measurableSet_Ioc] with x hx using by            simpa using mul_le_mul_of_nonneg_right (hbdd.choose_spec x hx)              (norm_nonneg (deriv g x))      convert hintFg using 1  simp_all only [sub_sub_cancel_left, norm_neg, Set.mem_Icc, ge_iff_le]  rw [← integral_const_mul]  refine le_trans (norm_integral_le_integral_norm _) (integral_mono_of_nonneg ?_ ?_ ?_)  · exact Eventually.of_forall fun x ↦ norm_nonneg _  · refine Integrable.const_mul ?_ _    have hderivint : IntegrableOn (deriv g) (Ioo a b) := by      have hcont := hg.continuousOn_derivWithin (uniqueDiffOn_Icc hab) le_rfl      exact (hcont.integrableOn_Icc.mono_set Ioo_subset_Icc_self) |> fun h ↦ h.congr_fun        (fun x hx ↦ by rw [derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)]) measurableSet_Ioo    simpa only [IntegrableOn, Measure.restrict_congr_set Ioo_ae_eq_Icc] using hderivint.abs  · filter_upwards [ae_restrict_mem measurableSet_Icc] with t ht    refine le_trans ?_ (mul_le_mul_of_nonneg_right (le_ciSup ?_ t) (abs_nonneg _))    · aesop    · obtain ⟨M, hM⟩ := IsCompact.exists_bound_of_continuousOn isCompact_Icc hF.continuousOn.norm      exact ⟨Max.max M 1, Set.forall_mem_range.mpr fun t ↦ by rw [ciSup_eq_ite]; aesop⟩