# mathlib3documentation

analysis.mellin_transform

# The Mellin transform #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the Mellin transform of a locally integrable function on Ioi 0, and show it is differentiable in a suitable vertical strip.

## Main statements #

• mellin : the Mellin transform ∫ (t : ℝ) in Ioi 0, t ^ (s - 1) • f t, where s is a complex number.
• has_mellin: shorthand asserting that the Mellin transform exists and has a given value (analogous to has_sum).
• mellin_differentiable_at_of_is_O_rpow : if f is O(x ^ (-a)) at infinity, and O(x ^ (-b)) at 0, then mellin f is holomorphic on the domain b < re s < a.
theorem complex.cpow_mul_of_real_nonneg {x : } (hx : 0 x) (y : ) (z : ) :
x ^ (y * z) = (x ^ y) ^ z
def mellin_convergent {E : Type u_1} [ E] (f : E) (s : ) :
Prop

Predicate on f and s asserting that the Mellin integral is well-defined.

Equations
theorem mellin_convergent.const_smul {E : Type u_1} [ E] {f : E} {s : } (hf : s) {𝕜 : Type u_2} [ E] [ E] (c : 𝕜) :
mellin_convergent (λ (t : ), c f t) s
theorem mellin_convergent.cpow_smul {E : Type u_1} [ E] {f : E} {s a : } :
mellin_convergent (λ (t : ), t ^ a f t) s (s + a)
theorem mellin_convergent.div_const {f : } {s : } (hf : s) (a : ) :
mellin_convergent (λ (t : ), f t / a) s
theorem mellin_convergent.comp_mul_left {E : Type u_1} [ E] {f : E} {s : } {a : } (ha : 0 < a) :
mellin_convergent (λ (t : ), f (a * t)) s
theorem mellin_convergent.comp_rpow {E : Type u_1} [ E] {f : E} {s : } {a : } (ha : a 0) :
mellin_convergent (λ (t : ), f (t ^ a)) s (s / a)
noncomputable def mellin {E : Type u_1} [ E] (f : E) (s : ) :
E

The Mellin transform of a function f (for a complex exponent s), defined as the integral of t ^ (s - 1) • f over Ioi 0.

Equations
theorem mellin_cpow_smul {E : Type u_1} [ E] (f : E) (s a : ) :
mellin (λ (t : ), t ^ a f t) s = (s + a)
theorem mellin_const_smul {E : Type u_1} [ E] (f : E) (s : ) {𝕜 : Type u_2} [ E] [ E] (c : 𝕜) :
mellin (λ (t : ), c f t) s = c s
theorem mellin_div_const (f : ) (s a : ) :
mellin (λ (t : ), f t / a) s = s / a
theorem mellin_comp_rpow {E : Type u_1} [ E] (f : E) (s : ) {a : } (ha : a 0) :
mellin (λ (t : ), f (t ^ a)) s = |a|⁻¹ (s / a)
theorem mellin_comp_mul_left {E : Type u_1} [ E] (f : E) (s : ) {a : } (ha : 0 < a) :
mellin (λ (t : ), f (a * t)) s = a ^ -s s
theorem mellin_comp_mul_right {E : Type u_1} [ E] (f : E) (s : ) {a : } (ha : 0 < a) :
mellin (λ (t : ), f (t * a)) s = a ^ -s s
theorem mellin_comp_inv {E : Type u_1} [ E] (f : E) (s : ) :
mellin (λ (t : ), f t⁻¹) s = (-s)
def has_mellin {E : Type u_1} [ E] (f : E) (s : ) (m : E) :
Prop

Predicate standing for "the Mellin transform of f is defined at s and equal to m". This shortens some arguments.

Equations
theorem has_mellin_add {E : Type u_1} [ E] {f g : E} {s : } (hf : s) (hg : s) :
has_mellin (λ (t : ), f t + g t) s (mellin f s + s)
theorem has_mellin_sub {E : Type u_1} [ E] {f g : E} {s : } (hf : s) (hg : s) :
has_mellin (λ (t : ), f t - g t) s (mellin f s - s)

## Convergence of Mellin transform integrals #

Auxiliary lemma to reduce convergence statements from vector-valued functions to real scalar-valued functions.

theorem mellin_convergent_top_of_is_O {f : } {a s : } (hf : f =O[filter.at_top] λ (t : ), t ^ -a) (hs : s < a) :

If f is a locally integrable real-valued function which is O(x ^ (-a)) at ∞, then for any s < a, its Mellin transform converges on some neighbourhood of +∞.

theorem mellin_convergent_zero_of_is_O {b : } {f : } (hf : f =O[ (set.Ioi 0)] λ (t : ), t ^ -b) {s : } (hs : b < s) :

If f is a locally integrable real-valued function which is O(x ^ (-b)) at 0, then for any b < s, its Mellin transform converges on some right neighbourhood of 0.

theorem mellin_convergent_of_is_O_scalar {a b : } {f : } {s : } (hf_top : f =O[filter.at_top] λ (t : ), t ^ -a) (hs_top : s < a) (hf_bot : f =O[ (set.Ioi 0)] λ (t : ), t ^ -b) (hs_bot : b < s) :

If f is a locally integrable real-valued function on Ioi 0 which is O(x ^ (-a)) at ∞ and O(x ^ (-b)) at 0, then its Mellin transform integral converges for b < s < a.

theorem mellin_convergent_of_is_O_rpow {E : Type u_1} [ E] {a b : } {f : E} {s : } (hf_top : f =O[filter.at_top] λ (t : ), t ^ -a) (hs_top : s.re < a) (hf_bot : f =O[ (set.Ioi 0)] λ (t : ), t ^ -b) (hs_bot : b < s.re) :
theorem is_O_rpow_top_log_smul {E : Type u_1} [ E] {a b : } {f : E} (hab : b < a) (hf : f =O[filter.at_top] λ (t : ), t ^ -a) :
(λ (t : ), f t) =O[filter.at_top] λ (t : ), t ^ -b

If f is O(x ^ (-a)) as x → +∞, then log • f is O(x ^ (-b)) for every b < a.

theorem is_O_rpow_zero_log_smul {E : Type u_1} [ E] {a b : } {f : E} (hab : a < b) (hf : f =O[ (set.Ioi 0)] λ (t : ), t ^ -a) :
(λ (t : ), f t) =O[ (set.Ioi 0)] λ (t : ), t ^ -b

If f is O(x ^ (-a)) as x → 0, then log • f is O(x ^ (-b)) for every a < b.

theorem mellin_has_deriv_of_is_O_rpow {E : Type u_1} [ E] {a b : } {f : E} {s : } (hf_top : f =O[filter.at_top] λ (t : ), t ^ -a) (hs_top : s.re < a) (hf_bot : f =O[ (set.Ioi 0)] λ (t : ), t ^ -b) (hs_bot : b < s.re) :
mellin_convergent (λ (t : ), f t) s (mellin (λ (t : ), f t) s) s

Suppose f is locally integrable on (0, ∞), is O(x ^ (-a)) as x → ∞, and is O(x ^ (-b)) as x → 0. Then its Mellin transform is differentiable on the domain b < re s < a, with derivative equal to the Mellin transform of log • f.

theorem mellin_differentiable_at_of_is_O_rpow {E : Type u_1} [ E] {a b : } {f : E} {s : } (hf_top : f =O[filter.at_top] λ (t : ), t ^ -a) (hs_top : s.re < a) (hf_bot : f =O[ (set.Ioi 0)] λ (t : ), t ^ -b) (hs_bot : b < s.re) :
s

Suppose f is locally integrable on (0, ∞), is O(x ^ (-a)) as x → ∞, and is O(x ^ (-b)) as x → 0. Then its Mellin transform is differentiable on the domain b < re s < a.

theorem mellin_convergent_of_is_O_rpow_exp {E : Type u_1} [ E] {a b : } (ha : 0 < a) {f : E} {s : } (hf_top : f =O[filter.at_top] λ (t : ), rexp (-a * t)) (hf_bot : f =O[ (set.Ioi 0)] λ (t : ), t ^ -b) (hs_bot : b < s.re) :

If f is locally integrable, decays exponentially at infinity, and is O(x ^ (-b)) at 0, then its Mellin transform converges for b < s.re.

theorem mellin_differentiable_at_of_is_O_rpow_exp {E : Type u_1} [ E] {a b : } (ha : 0 < a) {f : E} {s : } (hf_top : f =O[filter.at_top] λ (t : ), rexp (-a * t)) (hf_bot : f =O[ (set.Ioi 0)] λ (t : ), t ^ -b) (hs_bot : b < s.re) :
s

If f is locally integrable, decays exponentially at infinity, and is O(x ^ (-b)) at 0, then its Mellin transform is holomorphic on b < s.re.

## Mellin transforms of functions on Ioc 0 1#

theorem has_mellin_one_Ioc {s : } (hs : 0 < s.re) :
has_mellin ((set.Ioc 0 1).indicator (λ (t : ), 1)) s (1 / s)

The Mellin transform of the indicator function of Ioc 0 1.

theorem has_mellin_cpow_Ioc (a : ) {s : } (hs : 0 < s.re + a.re) :
has_mellin ((set.Ioc 0 1).indicator (λ (t : ), t ^ a)) s (1 / (s + a))

The Mellin transform of a power function restricted to Ioc 0 1.