Mellin Of Smooth1a

@[blueprint  (title := "MellinOfSmooth1a")  (statement := /--  Fix  $\epsilon>0$. Then the Mellin transform of $\widetilde{1_{\epsilon}}$ is  $$\mathcal{M}(\widetilde{1_{\epsilon}})(s) =  \frac{1}{s}\left(\mathcal{M}(\nu)\left(\epsilon s\right)\right).$$  -/)  (proof := /--  By Definition \ref{Smooth1},  $$    \mathcal M(\widetilde{1_\epsilon})(s)    =\mathcal M(1_{(0,1]}\ast\nu_\epsilon)(s)    .  $$  We wish to apply Theorem \ref{MellinConvolutionTransform}.  To do so, we must prove that  $$    (x,y)\mapsto 1_{(0,1]}(y)\nu_\epsilon(x/y)/y  $$  is integrable on $[0,\infty)^2$.  It is actually easier to do this for the convolution: $\nu_\epsilon\ast 1_{(0,1]}$, so we use  Lemma \ref{MellinConvolutionSymmetric}: for $x\neq0$,  $$    1_{(0,1]}\ast\nu_\epsilon(x)=\nu_\epsilon\ast 1_{(0,1]}(x)    .  $$  Now, for $x=0$, both sides of the equation are 0, so the equation also holds for $x=0$.  Therefore,  $$    \mathcal M(\widetilde{1_\epsilon})(s)    =\mathcal M(\nu_\epsilon\ast 1_{(0,1]})(s)    .  $$  Now,  $$    (x,y)\mapsto \nu_\epsilon(y)1_{(0,1]}(x/y)\frac{x^{s-1}}y  $$  has compact support that is bounded away from $y=0$ (specifically  $y\in[2^{-\epsilon},2^\epsilon]$ and $x\in(0,y]$), so it is integrable.  We can thus apply Theorem \ref{MellinConvolutionTransform} and find  $$    \mathcal M(\widetilde{1_\epsilon})(s)    =\mathcal M(\nu_\epsilon)(s)\mathcal M(1_{(0,1]})(s)    .  $$  By Lemmas \ref{MellinOf1} and \ref{MellinOfDeltaSpike},  $$    \mathcal M(\widetilde{1_\epsilon})(s)    =\frac1s\mathcal M(\nu)(\epsilon s)    .  $$  -/)  (latexEnv := "lemma")]lemma MellinOfSmooth1a {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν)    (suppν : ν.support ⊆ Icc (1 / 2) 2)    {ε : ℝ} (εpos : 0 < ε) {s : ℂ} (hs : 0 < s.re) :    𝓜 (fun x ↦ (Smooth1 ν ε x : ℂ)) s =      s⁻¹ * 𝓜 (fun x ↦ (ν x : ℂ)) (ε * s) := by  let f' : ℝ → ℂ := fun x ↦ DeltaSpike ν ε x  let f : ℝ → ℂ := fun x ↦ DeltaSpike ν ε x / x  let g : ℝ → ℂ := fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0  let F : ℝ × ℝ → ℂ := Function.uncurry fun x y ↦ f y * g (x / y) * (x : ℂ) ^ (s - 1)  let S := {⟨x, y⟩ : ℝ × ℝ | 0 < x  ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}  let F' : ℝ × ℝ → ℂ := piecewise S (fun ⟨x, y⟩ ↦ f y * (x : ℂ) ^ (s - 1))     (fun _ ↦ 0)  let Tx := Ioc 0 ((2 : ℝ) ^ ε)  let Ty := Icc ((2 : ℝ) ^ (-ε)) ((2 : ℝ) ^ ε)   have Seq : S = (Tx ×ˢ Ty) ∩ {(x, y) : ℝ × ℝ | x ≤ y} := by    ext ⟨x, y⟩; constructor    · exact fun h ↦ ⟨⟨⟨h.1, le_trans h.2.1 h.2.2.2⟩, ⟨h.2.2.1, h.2.2.2⟩⟩, h.2.1⟩    · exact fun h ↦  ⟨h.1.1.1, ⟨h.2, h.1.2.1, h.1.2.2⟩⟩  have SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0 :=    fun z hz ↦ ⟨hz.1, lt_of_lt_of_le (by apply rpow_pos_of_pos; norm_num) hz.2.2.1⟩  have SsubT: S ⊆ Tx ×ˢ Ty := by simp_rw [Seq, inter_subset_left]  have Smeas : MeasurableSet S := by    rw [Seq]; apply MeasurableSet.inter ?_ <| measurableSet_le measurable_fst measurable_snd    simp [measurableSet_prod, Tx, Ty]   have int_F: IntegrableOn F (Ioi 0 ×ˢ Ioi 0) := by    apply IntegrableOn.congr_fun (f := F') ?_ ?_ (by simp [measurableSet_prod]); swap    · simp only [F, F', f, g, mul_ite, mul_one, mul_zero]      intro ⟨x, y⟩ hz      by_cases hS : ⟨x, y⟩ ∈ S <;> simp only [hS, piecewise]      <;> simp only [mem_prod, mem_Ioi, mem_setOf_eq, not_and, not_le, S] at hz hS      · simp [div_pos hz.1 hz.2, (div_le_one hz.2).mpr hS.2.1]      · by_cases hxy : x / y ≤ 1        swap        · simp [hxy]        have hy : y ∉ Icc (2 ^ (-ε)) (2 ^ ε) := by          simp only [mem_Icc, not_and, not_le]; exact hS hz.1 <| (div_le_one hz.2).mp hxy        simp [DeltaSpikeSupport εpos hz.2.le suppν hy]    · apply Integrable.piecewise Smeas ?_ integrableOn_zero      simp only [IntegrableOn, Measure.restrict_restrict_of_subset SsubI]      apply MeasureTheory.Integrable.mono_measure ?_      · apply MeasureTheory.Measure.restrict_mono' SsubT.eventuallyLE le_rfl      have : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty) := by        rw [Measure.prod_restrict, MeasureTheory.Measure.volume_eq_prod]      conv => rw [this]; lhs; intro; rw [mul_comm]      apply MeasureTheory.Integrable.mul_prod (f := fun x ↦ (x : ℂ) ^ (s - 1))        (μ := Measure.restrict volume Tx)      · simp only [Tx]        rw [← IntegrableOn, integrableOn_Ioc_iff_integrableOn_Ioo,          intervalIntegral.integrableOn_Ioo_cpow_iff]        · simp [hs]        · apply rpow_pos_of_pos (by norm_num)      · apply (ContinuousOn.div ?_ ?_ ?_).integrableOn_compact isCompact_Icc        · exact (DeltaSpikeOfRealContinuous εpos diffν).continuousOn        · exact continuous_ofReal.continuousOn        · intro x hx; simp only [mem_Icc] at hx; simp only [ofReal_ne_zero]          linarith [(by apply rpow_pos_of_pos (by norm_num) : (0 : ℝ) < 2 ^ (-ε))]   have : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s := by    rw [mul_comm, ← MellinConvolutionTransform f' g s      (by convert int_F using 1; simp only [f', F, f]; field_simp)]    dsimp [mellin]; rw [setIntegral_congr_fun (by simp)]    intro x hx; simp_rw [MellinConvolutionSymmetric _ _ <| mem_Ioi.mp hx]   convert! this using 1  · congr; funext x; convert! integral_ofReal.symm    simp only [MellinConvolution, RCLike.ofReal_div, ite_mul, one_mul, zero_mul, @apply_ite ℝ ℂ,      algebraMap.coe_zero, g]; rfl  · rw [MellinOf1 s hs, MellinOfDeltaSpike ν εpos s]    simp