mellin_eq_fourierIntegral — Mathlib

English

The Mellin transform of f equals the Fourier transform of a suitable exponential-modulated version of f.

Русский

Меллин-преобразование функции f равно Фурье-преобразованию соответствующей модуляции по экспоненте.

LaTeX

$$$\text{mellin}(f,s) = \mathcal{F}\big(u \mapsto e^{-s_{\mathrm{re}}u} f(e^{-u})\big)(s_{\mathrm{im}}/(2\pi))$$$

Lean4

theorem mellin_eq_fourierIntegral (f : ℝ → E) {s : ℂ} :
    mellin f s = 𝓕 (fun (u : ℝ) ↦ (Real.exp (-s.re * u) • f (Real.exp (-u)))) (s.im / (2 * π)) :=
  calc
    mellin f s = ∫ (u : ℝ), Complex.exp (-s * u) • f (Real.exp (-u)) :=
      by
      rw [mellin, ← rexp_neg_image_aux,
        integral_image_eq_integral_abs_deriv_smul MeasurableSet.univ rexp_neg_deriv_aux rexp_neg_injOn_aux]
      simp [rexp_cexp_aux]
    _ = ∫ (u : ℝ), Complex.exp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • (Real.exp (-s.re * u) • f (Real.exp (-u))) :=
      by
      congr
      ext u
      trans Complex.exp (-s.im * u * I) • (Real.exp (-s.re * u) • f (Real.exp (-u)))
      · conv => lhs; rw [← re_add_im s]
        rw [neg_add, add_mul, Complex.exp_add, mul_comm, ← smul_eq_mul, smul_assoc]
        norm_cast
        push_cast
        ring_nf
      congr
      simp [field]
    _ = 𝓕 (fun (u : ℝ) ↦ (Real.exp (-s.re * u) • f (Real.exp (-u)))) (s.im / (2 * π)) := by
      simp [fourierIntegral_eq', mul_comm (_ / _)]

Похожие утверждения