mellin_div_const — Mathlib

English

Dividing the integrand by a scalar within Mellin scales the transform by the reciprocal of that scalar.

Русский

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

LaTeX

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

Lean4

theorem mellin_div_const (f : ℝ → ℂ) (s a : ℂ) : mellin (fun t => f t / a) s = mellin f s / a := by
  simp_rw [mellin, smul_eq_mul, ← mul_div_assoc, integral_div]

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