MellinOfPsi

@[blueprint  (title := "MellinOfPsi")  (statement := /--  The Mellin transform of $\nu$ is  $$\mathcal{M}(\nu)(s) =  O\left(\frac{1}{|s|}\right),$$  as $|s|\to\infty$ with $\sigma_1 \le \Re(s) \le 2$.  -/)  (proof := /--  Integrate by parts:  $$  \left|\int_0^\infty \nu(x)x^s\frac{dx}{x}\right| =  \left|-\int_0^\infty \nu'(x)\frac{x^{s}}{s}dx\right|  $$  $$  \le \frac{1}{|s|} \int_{1/2}^2|\nu'(x)|x^{\Re(s)}dx.  $$  Since $\Re(s)$ is bounded, the right-hand side is bounded by a  constant times $1/|s|$.  -/)]lemma MellinOfPsi {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν)    (suppν : ν.support ⊆ Set.Icc (1 / 2) 2) :    ∃ C > 0, ∀ (σ₁ : ℝ) (_ : 0 < σ₁) (s : ℂ) (_ : σ₁ ≤ s.re) (_ : s.re ≤ 2),    ‖𝓜 (fun x ↦ (ν x : ℂ)) s‖ ≤ C * ‖s‖⁻¹ := by  let f := fun (x : ℝ) ↦ ‖deriv ν x‖  have cont : ContinuousOn f (Icc (1 / 2) 2) :=    (Continuous.comp (by continuity) <| diffν.continuous_deriv (by norm_num)).continuousOn  obtain ⟨a, _, max⟩ := isCompact_Icc.exists_isMaxOn (f := f) (by norm_num) cont  let σ₂ : ℝ := 2  let C : ℝ := f a * 2 ^ σ₂ * (3 / 2)  have mainBnd : ∀ (σ₁ : ℝ), 0 < σ₁ → ∀ (s : ℂ), σ₁ ≤ s.re → s.re ≤ 2 →      ‖𝓜 (fun x ↦ (ν x : ℂ)) s‖ ≤ C * ‖s‖⁻¹ := by    intro σ₁ σ₁pos s hs₁ hs₂    have s_ne_zero: s ≠ 0 := fun h ↦ by linarith [zero_re ▸ h ▸ hs₁]    simp only [mellin, f, MellinOfPsi_aux diffν suppν s_ne_zero, norm_mul, smul_eq_mul, mul_comm]    gcongr    · simp    calc      _ ≤ ∫ (x : ℝ) in Ioi 0, ‖(deriv ν x * (x : ℂ) ^ s)‖ := ?_      _ = ∫ (x : ℝ) in Icc (1 / 2) 2, ‖(deriv ν x * (x : ℂ) ^ s)‖ := ?_      _ ≤ ‖∫ (x : ℝ) in Icc (1 / 2) 2, ‖(deriv ν x * (x : ℂ) ^ s)‖‖ :=          le_abs_self _      _ ≤ _ := ?_    · simp_rw [norm_integral_le_integral_norm]    · apply SetIntegral.integral_eq_integral_inter_of_support_subset_Icc      · simp only [Function.support_abs, Function.support_mul, Function.support_ofReal]        apply subset_trans (by apply inter_subset_left) <| Function.support_deriv_subset_Icc suppν      · exact (Icc_subset_Ioi_iff (by norm_num)).mpr (by norm_num)    · have := intervalIntegral.norm_integral_le_of_norm_le_const' (C := f a * 2 ^ σ₂)        (f := fun x ↦ f x * ‖(x : ℂ) ^ s‖) (a := (1 / 2 : ℝ)) ( b := 2) (by norm_num) ?_      · simp only [Real.norm_eq_abs, norm_real, norm_mul] at this ⊢        rwa [(by norm_num: |(2 : ℝ) - 1 / 2| = 3 / 2),            intervalIntegral.integral_of_le (by norm_num), ← integral_Icc_eq_integral_Ioc] at this      · intro x hx;        have f_bound := isMaxOn_iff.mp max x hx        have pow_bound : ‖(x : ℂ) ^ s‖ ≤ 2 ^ σ₂ := by          rw [norm_cpow_eq_rpow_re_of_pos (by linarith [mem_Icc.mp hx])]          have xpos : 0 ≤ x := by linarith [(mem_Icc.mp hx).1]          have h := rpow_le_rpow xpos (mem_Icc.mp hx).2 (by linarith : 0 ≤ s.re)          exact le_trans h <| rpow_le_rpow_of_exponent_le (by norm_num) hs₂        convert! mul_le_mul f_bound pow_bound (norm_nonneg _) ?_ using 1 <;> simp [f]  have Cnonneg : 0 ≤ C := by    have hh := mainBnd 1 (by norm_num) ((3 : ℂ) / 2) (by norm_num) (by norm_num)    have hhh : 0 ≤ ‖𝓜 (fun x ↦ (ν x : ℂ)) ((3 : ℂ) / 2)‖ := by positivity    have hhhh : 0 < ‖(3 : ℂ) / 2‖⁻¹ := by norm_num    have := hhh.trans hh    exact (mul_nonneg_iff_of_pos_right hhhh).mp this  by_cases CeqZero : C = 0  · refine ⟨1, by linarith, ?_⟩    intro ε εpos s hs₁ hs₂    have := mainBnd ε εpos s hs₁ hs₂    rw [CeqZero, zero_mul] at this    have : 0 ≤ 1 * ‖s‖⁻¹ := by positivity    linarith  · exact ⟨C, lt_of_le_of_ne Cnonneg fun a ↦ CeqZero (id (Eq.symm a)), mainBnd⟩