div_const — Mathlib

English

Dividing the integrand inside Mellin by a scalar a corresponds to dividing the Mellin transform by a.

Русский

Деление внутри интеграла Меллина на константу a эквивалентно делению самого преобразования Меллина на a.

LaTeX

$$$\text{mellin}(f,s) / a = \text{mellin}(f/a,s)$$$

Lean4

nonrec theorem div_const {f : ℝ → ℂ} {s : ℂ} (hf : MellinConvergent f s) (a : ℂ) :
    MellinConvergent (fun t => f t / a) s := by
  simpa only [MellinConvergent, smul_eq_mul, ← mul_div_assoc] using hf.div_const a

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