English
If f is Mellin-convergent and certain integrability conditions hold, then mellinInv of mellin f recovers f on x>0.
Русский
Если функция f удовлетворяет условиям сходимости Меллина и интегрируемости, то mellinInv(меллин f) восстанавливает f на x>0.
LaTeX
$$$\forall \sigma, f, x>0:\ mellinInv(\sigma, \mathrm{mellin}(f))(x) = f(x)$ under the standard convergence hypotheses$$
Lean4
/-- The inverse Mellin transform of the Mellin transform applied to `x > 0` is x. -/
theorem mellin_inversion (σ : ℝ) (f : ℝ → E) {x : ℝ} (hx : 0 < x) (hf : MellinConvergent f σ)
(hFf : VerticalIntegrable (mellin f) σ) (hfx : ContinuousAt f x) : mellinInv σ (mellin f) x = f x :=
by
let g := fun (u : ℝ) => Real.exp (-σ * u) • f (Real.exp (-u))
replace hf : Integrable g :=
by
rw [MellinConvergent, ← rexp_neg_image_aux,
integrableOn_image_iff_integrableOn_abs_deriv_smul MeasurableSet.univ rexp_neg_deriv_aux rexp_neg_injOn_aux] at hf
replace hf : Integrable fun (x : ℝ) ↦ cexp (-↑σ * ↑x) • f (rexp (-x)) := by simpa [rexp_cexp_aux] using hf
norm_cast at hf
replace hFf : Integrable (𝓕 g) := by
have h2π : 2 * π ≠ 0 := by simp
have : Integrable (𝓕 (fun u ↦ rexp (-(σ * u)) • f (rexp (-u)))) := by
simpa [mellin_eq_fourierIntegral, mul_div_cancel_right₀ _ h2π] using hFf.comp_mul_right' h2π
simp_rw [neg_mul_eq_neg_mul] at this
exact this
replace hfx : ContinuousAt g (-Real.log x) :=
by
refine ContinuousAt.smul (by fun_prop) (ContinuousAt.comp ?_ (by fun_prop))
simpa [Real.exp_log hx] using hfx
calc
mellinInv σ (mellin f) x = mellinInv σ (fun s ↦ 𝓕 g (s.im / (2 * π))) x := by
simp [g, mellinInv, mellin_eq_fourierIntegral]
_ = (x : ℂ) ^ (-σ : ℂ) • g (-Real.log x) :=
by
rw [mellinInv_eq_fourierIntegralInv _ _ hx, ← hf.fourier_inversion hFf hfx]
simp [mul_div_cancel_left₀ _ (show 2 * π ≠ 0 by simp)]
_ = (x : ℂ) ^ (-σ : ℂ) • rexp (σ * Real.log x) • f (rexp (Real.log x)) := by simp [g]
_ = f x := by
norm_cast
rw [mul_comm σ, ← rpow_def_of_pos hx, Real.exp_log hx, ← Complex.ofReal_cpow hx.le]
norm_cast
rw [← smul_assoc, smul_eq_mul, Real.rpow_neg hx.le, inv_mul_cancel₀ (ne_of_gt (rpow_pos_of_pos hx σ)), one_smul]
