mellinInv_eq_fourierIntegralInv — Mathlib

English

Inverse Mellin transform of the inverse Fourier representation recovers the original function up to a power of x.

Русский

Обратное преобразование Меллина в комбинации с Фурье восстанавливает исходную функцию (с множителем степени x).

LaTeX

$$$\text{mellinInv}(\sigma,f,x) = x^{-\sigma} \cdot \mathcal{F}^{-1}\big( f(\sigma + 2\pi yi)\big)(-\log x)$$$

Lean4

theorem mellinInv_eq_fourierIntegralInv (σ : ℝ) (f : ℂ → E) {x : ℝ} (hx : 0 < x) :
    mellinInv σ f x = (x : ℂ) ^ (-σ : ℂ) • 𝓕⁻ (fun (y : ℝ) ↦ f (σ + 2 * π * y * I)) (-Real.log x) :=
  calc
    mellinInv σ f x =
        (x : ℂ) ^ (-σ : ℂ) • (∫ (y : ℝ), Complex.exp (2 * π * (y * (-Real.log x)) * I) • f (σ + 2 * π * y * I)) :=
      by
      rw [mellinInv, one_div, ← abs_of_pos (show 0 < (2 * π)⁻¹ by simp [pi_pos])]
      have hx0 : (x : ℂ) ≠ 0 := ofReal_ne_zero.mpr (ne_of_gt hx)
      simp_rw [neg_add, cpow_add _ _ hx0, mul_smul, integral_smul]
      rw [smul_comm, ← Measure.integral_comp_mul_left]
      congr! 3
      rw [cpow_def_of_ne_zero hx0, ← Complex.ofReal_log hx.le]
      push_cast
      ring_nf
    _ = (x : ℂ) ^ (-σ : ℂ) • 𝓕⁻ (fun (y : ℝ) ↦ f (σ + 2 * π * y * I)) (-Real.log x) := by
      simp [fourierIntegralInv_eq', mul_comm (Real.log _)]

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