Theorems · Theorem · integral transforms

mellin_comp_rpow

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) (a : ℝ),
  mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)

Defined in

Mathlib.Analysis.MellinTransform

Cited by

1 results in Mathlib

Foundations

Depth 283 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace