HasMellin — Mathlib

English

HasMellin f s m means that the Mellin transform converges at s and equals m.

Русский

HasMellin f s m означает, что преобразование Меллина сходится в точке s и равно m.

LaTeX

$$$\text{HasMellin}(f,s,m) \;\iff\; \text{MellinConvergent}(f,s) \wedge \operatorname{mellin}(f)(s) = m.$$$

Lean4

/-- Predicate standing for "the Mellin transform of `f` is defined at `s` and equal to `m`". This
shortens some arguments. -/
def HasMellin (f : ℝ → E) (s : ℂ) (m : E) : Prop :=
  MellinConvergent f s ∧ mellin f s = m

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