ZetaAppendix.lemma_IBP_bound_abs_antitone

theorem lemma_IBP_bound_abs_antitone {a b : ℝ} (hab : a < b) (g : ℝ → ℝ) (F : ℝ → ℂ)    (hgcont : ContinuousOn g (Icc a b)) (hganti : AntitoneOn (|g ·|) (Icc a b))    (hF : ContDiffOn ℝ 1 F (Icc a b)) :    ‖∫ t in Icc a b, (g t : ℂ) * deriv F t‖ ≤ (⨆ t ∈ Icc a b, ‖F t‖) * (2 * |g a|) := by  have hsign : (∀ t ∈ Icc a b, g t ≥ 0) ∨ (∀ t ∈ Icc a b, g t ≤ 0) := by    by_cases hsign : ∃ a' b' : ℝ, a ≤ a' ∧ a' < b' ∧ b' ≤ b ∧ g a' * g b' < 0    · obtain ⟨a', b', ha', hb', hab', hsign⟩ := hsign      obtain ⟨r, hr⟩ : ∃ r ∈ Icc a' b', g r = 0 := by        have hivt : ContinuousOn g (Icc a' b') := hgcont.mono (Icc_subset_Icc ha' hab')        have := hivt.image_Icc hb'.le        exact this.symm.subset (Set.mem_Icc.mpr ⟨by nlinarith [Set.mem_Icc.mp (this ▸          mem_image_of_mem g (Set.left_mem_Icc.mpr hb'.le)), Set.mem_Icc.mp (this ▸          mem_image_of_mem g (Set.right_mem_Icc.mpr hb'.le))], by nlinarith [mem_Icc.mp (this ▸          mem_image_of_mem g (Set.left_mem_Icc.mpr hb'.le)), mem_Icc.mp (this ▸          mem_image_of_mem g (Set.right_mem_Icc.mpr hb'.le))]⟩)      have := hganti ⟨by linarith [hr.1.1], by linarith [hr.1.2]⟩ ⟨by linarith [hr.1.1], by        linarith [hr.1.2]⟩ hr.1.2      simp_all    · contrapose! hsign      obtain ⟨⟨x, hx₁, hx₂⟩, ⟨y, hy₁, hy₂⟩⟩ := hsign      norm_num at *      cases lt_or_gt_of_ne (show x ≠ y by rintro rfl; linarith) with      | inl h => exact ⟨x, hx₁.1, y, by linarith, by linarith, by nlinarith⟩      | inr h => exact ⟨y, hy₁.1, x, by linarith, by linarith, by nlinarith⟩  cases hsign with  | inl hsign =>    have hbd₁ : ‖(∫ 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 a - g b) := by      have := @lemma_IBP_bound_monotone a b hab (fun t ↦ -g t) F ?_ ?_ ?_ <;> norm_num at *      · convert this using 1 <;> norm_num [integral_neg]        · ring_nf; rw [← norm_neg]; ring_nf        · exact Or.inl <| by ring      · exact hgcont.neg      · intro t ht u hu htu; have := hganti ht hu htu; simp_all [abs_of_nonneg]      · assumption    have hbd₂ : ‖g b * F b - g a * F a‖ ≤ (⨆ t ∈ Icc a b, ‖F t‖) * (g b + g a) := by      refine (norm_sub_le _ _).trans ?_      have hFle : ∀ t ∈ Icc a b, ‖F t‖ ≤ ⨆ t ∈ Icc a b, ‖F t‖ := fun t ht ↦ by        apply le_csSup        · obtain ⟨M, hM⟩ := IsCompact.exists_bound_of_continuousOn isCompact_Icc hF.continuousOn          exact ⟨max M 1, forall_mem_range.mpr fun t ↦ by rw [ciSup_eq_ite]; aesop⟩        · exact ⟨t, by simp_all⟩      norm_num at *      rw [abs_of_nonneg (hsign b hab.le le_rfl), abs_of_nonneg (hsign a le_rfl hab.le)]      nlinarith [hFle b hab.le le_rfl, hFle a le_rfl hab.le, hsign b hab.le le_rfl, hsign a le_rfl hab.le]    have hbd₃ : ‖∫ t in Icc a b, (g t : ℂ) * deriv F t‖ ≤        (⨆ t ∈ Icc a b, ‖F t‖) * (g a - g b) + (⨆ t ∈ Icc a b, ‖F t‖) * (g b + g a) := by      have h := norm_add_le ((∫ t in Icc a b, (g t : ℂ) * deriv F t) -        (g b * F b - g a * F a)) (g b * F b - g a * F a)      simpa using h.trans (add_le_add hbd₁ hbd₂)    exact hbd₃.trans (by      rw [abs_of_nonneg (hsign a <| left_mem_Icc.mpr hab.le)]      nlinarith [show 0 ≤ ⨆ t ∈ Icc a b, ‖F t‖ from iSup_nonneg fun _ ↦ iSup_nonneg fun _ ↦ norm_nonneg _])  | inr hsign =>    have hbd₁ : ‖(∫ 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      apply_rules [lemma_IBP_bound_monotone]      intro x hx y hy hxy; have := hganti hx hy hxy; simp_all [abs_of_nonpos]    have hbd₂ : ‖g b * F b - g a * F a‖ ≤ (⨆ t ∈ Icc a b, ‖F t‖) * (|g b| + |g a|) := by      have hFle : ∀ t ∈ Icc a b, ‖F t‖ ≤ ⨆ t ∈ Icc a b, ‖F t‖ := fun t ht ↦ by        apply le_csSup        · obtain ⟨M, hM⟩ := IsCompact.exists_bound_of_continuousOn isCompact_Icc hF.continuousOn.norm          use max M 1          rintro x ⟨t, rfl⟩; by_cases ht : t ∈ Icc a b <;> simp_all        · exact ⟨t, by simp_all⟩      refine (norm_sub_le ..).trans ?_      simp only [Set.mem_Icc, and_imp, norm_mul, norm_real, norm_eq_abs] at *      nlinarith [abs_nonneg (g b), abs_nonneg (g a),        hFle b (by linarith) (by linarith), hFle a (by linarith) (by linarith)]    have hbd₃ : ‖∫ t in Icc a b, (g t : ℂ) * deriv F t‖ ≤        (⨆ t ∈ Icc a b, ‖F t‖) * (g b - g a) + (⨆ t ∈ Icc a b, ‖F t‖) * (|g b| + |g a|) := by      have h := norm_add_le ((∫ t in Icc a b, (g t : ℂ) * deriv F t) - (g b * F b - g a * F a)) (g b * F b - g a * F a)      simpa using h.trans (add_le_add hbd₁ hbd₂)    convert hbd₃ using 1    rw [abs_of_nonpos (hsign b <| right_mem_Icc.mpr hab.le), abs_of_nonpos (hsign a <| left_mem_Icc.mpr hab.le)]    ring