second_fourier

@[blueprint "second-fourier"  (title := "second-fourier")  (statement := /--  If $\psi: \R \to \C$ is absolutely integrable and $x > 0$, then for any $\sigma>1$  $$ \int_{-\log x}^\infty e^{-u(\sigma-1)} \hat \psi(\frac{u}{2\pi})\ du =  x^{\sigma - 1} \int_\R \frac{1}{\sigma+it-1} \psi(t) x^{it}\ dt.$$  -/)  (proof := /--  The left-hand side expands as  $$ \int_{-\log x}^\infty \int_\R e^{-u(\sigma-1)} \psi(t) e(-\frac{tu}{2\pi})\ dt\ du$$  so by Fubini's theorem it suffices to verify the identity  \begin{align*}  \int_{-\log x}^\infty e^{-u(\sigma-1)} e(-\frac{tu}{2\pi})\ du  &= \int_{-\log x}^\infty e^{(it - \sigma + 1)u}\ du \\  &= \frac{1}{it - \sigma + 1} e^{(it - \sigma + 1)u}\ \Big|_{-\log x}^\infty \\  &= x^{\sigma - 1} \frac{1}{\sigma+it-1} x^{it}  \end{align*}  -/)  (latexEnv := "lemma")]lemma second_fourier (hcont : Measurable ψ) (hsupp : Integrable ψ)    {x σ' : ℝ} (hx : 0 < x) (hσ : 1 < σ') :    ∫ u in Ici (-log x), Real.exp (-u * (σ' - 1)) * 𝓕 (ψ : ℝ → ℂ) (u / (2 * π)) =    (x^(σ' - 1) : ℝ) * ∫ t, (1 / (σ' + t * I - 1)) * ψ t * x^(t * I) ∂ volume := by   conv in ↑(rexp _) * _ => { rw [Real.fourier_real_eq, ← smul_eq_mul, ← integral_smul] }  rw [MeasureTheory.integral_integral_swap]  swap  · exact second_fourier_integrable_aux1 hcont hsupp hσ  rw [← integral_const_mul]  congr 1; ext t  dsimp [Real.fourierChar, Circle.exp]   simp_rw [mul_smul_comm, ← smul_mul_assoc, integral_mul_const]  rw [fun (a b d : ℂ) ↦ show a * (b * (ψ t) * d) = (a * b * d) * ψ t by ring]  congr 1  conv =>    lhs    enter [2]    ext a    rw [AddChar.coe_mk, Submonoid.mk_smul, smul_eq_mul]  push_cast  simp_rw [← Complex.exp_add]  have (u : ℝ) :      2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I + -↑u * (↑σ' - 1) = (1 - σ' - t * I) * u := calc    _ = -↑u * (↑σ' - 1) + (2 * ↑π) / (2 * ↑π) * -(↑t * ↑u) * I := by ring    _ = -↑u * (↑σ' - 1) + 1 * -(↑t * ↑u) * I := by rw [div_self (by norm_num)]    _ = _ := by ring  simp_rw [this]  let c : ℂ := (1 - ↑σ' - ↑t * I)  have : c ≠ 0 := by simp [Complex.ext_iff, c, sub_ne_zero.mpr hσ.ne]  let f' (u : ℝ) := cexp (c * u)  let f := fun (u : ℝ) ↦ (f' u) / c  have hderiv : ∀ u ∈ Ici (-Real.log x), HasDerivAt f (f' u) u := by    intro u _    rw [show f' u = cexp (c * u) * (c * 1) / c by simp only [f']; field_simp]    exact (hasDerivAt_id' u).ofReal_comp.const_mul c |>.cexp.div_const c  have hf : Tendsto f atTop (𝓝 0) := by    apply tendsto_zero_iff_norm_tendsto_zero.mpr    suffices Tendsto (fun (x : ℝ) ↦ ‖cexp (c * ↑x)‖ / ‖c‖) atTop (𝓝 (0 / ‖c‖)) by      simpa [f, f'] using this    apply Filter.Tendsto.div_const    suffices Tendsto (· * (1 - σ')) atTop atBot by simpa [Complex.norm_exp, mul_comm (1 - σ'), c]    exact Tendsto.atTop_mul_const_of_neg (by linarith) fun ⦃s⦄ h ↦ h  rw [integral_Ici_eq_integral_Ioi,    integral_Ioi_of_hasDerivAt_of_tendsto' hderiv (second_fourier_integrable_aux2 hσ) hf]  simpa [f, f'] using second_fourier_aux hx