hasMellin — Mathlib

English

The Mellin transform of f agrees with the Λ-function for all complex s, i.e., Λ(s) = mellin f(s).

Русский

Меллина-преобразование f совпадает с функцией Λ: Λ(s) = mellin f(s) для всех комплексных s.

LaTeX

$$Λ = mellin P.f$$

Lean4

/-- The Mellin transform of `f` is well-defined and equal to `P.Λ s`, for all `s`. -/
theorem hasMellin (s : ℂ) : HasMellin P.f s (P.Λ s) :=
  let ⟨_, ht⟩ := exists_gt s.re
  let ⟨_, hu⟩ := exists_lt s.re
  ⟨mellinConvergent_of_isBigO_rpow P.hf_int (P.hf_top' _) ht (P.hf_zero' _) hu, rfl⟩

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