Complex powers on the positive half-line

This scalar calculus has no simplex dependency. The historical DirichletTransform namespace is retained for compatibility.

noncomputable def DirichletTransform.positiveCpow (a : ℂ) (x : ℝ) : ℂ

A complex power on the positive half-line, extended by zero.

Equations

• DirichletTransform.positiveCpow a x = if 0 < x then ↑x ^ a else 0

theorem DirichletTransform.continuous_positiveCpow {a : ℂ} (ha : 0 < a.re) : Continuous (positiveCpow a)

theorem DirichletTransform.hasDerivAt_positiveCpow {a : ℂ} (ha : 1 < a.re) (x : ℝ) : HasDerivAt (positiveCpow a) (a * positiveCpow (a - 1) x) x

noncomputable def DirichletTransform.positiveGammaPower (a : ℂ) (x : ℝ) : ℂ

The normalized positive power; differentiation lowers the parameter by one.

Equations

• DirichletTransform.positiveGammaPower a x = DirichletTransform.positiveCpow (a - 1) x / Complex.Gamma a

theorem DirichletTransform.continuous_positiveGammaPower {a : ℂ} (ha : 1 < a.re) : Continuous (positiveGammaPower a)

theorem DirichletTransform.hasDerivAt_positiveGammaPower {a : ℂ} (ha : 2 < a.re) (x : ℝ) : HasDerivAt (positiveGammaPower a) (positiveGammaPower (a - 1) x) x