Theorems · Theorem · integral transforms

MellinConvergent.comp_rpow

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {s : ℂ} {a : ℝ},
  a ≠ 0 → (MellinConvergent (fun t => f (t ^ a)) s ↔ MellinConvergent f (s / ↑a))

Defined in

Mathlib.Analysis.MellinTransform

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace