mathlib3 documentation

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 #

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} [normed_add_comm_group E] [normed_space 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} [normed_add_comm_group E] [normed_space E] {f : E} {s : } (hf : mellin_convergent f s) {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [smul_comm_class 𝕜 E] (c : 𝕜) :
mellin_convergent (λ (t : ), c f t) s
theorem mellin_convergent.cpow_smul {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E} {s a : } :
mellin_convergent (λ (t : ), t ^ a f t) s mellin_convergent f (s + a)
theorem mellin_convergent.div_const {f : } {s : } (hf : mellin_convergent f s) (a : ) :
mellin_convergent (λ (t : ), f t / a) s
theorem mellin_convergent.comp_mul_left {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E} {s : } {a : } (ha : 0 < a) :
mellin_convergent (λ (t : ), f (a * t)) s mellin_convergent f s
theorem mellin_convergent.comp_rpow {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E} {s : } {a : } (ha : a 0) :
mellin_convergent (λ (t : ), f (t ^ a)) s mellin_convergent f (s / a)
noncomputable def mellin {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space 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} [normed_add_comm_group E] [normed_space E] [complete_space E] (f : E) (s a : ) :
mellin (λ (t : ), t ^ a f t) s = mellin f (s + a)
theorem mellin_const_smul {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] (f : E) (s : ) {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [smul_comm_class 𝕜 E] (c : 𝕜) :
mellin (λ (t : ), c f t) s = c mellin f s
theorem mellin_div_const (f : ) (s a : ) :
mellin (λ (t : ), f t / a) s = mellin f s / a
theorem mellin_comp_rpow {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] (f : E) (s : ) {a : } (ha : a 0) :
mellin (λ (t : ), f (t ^ a)) s = |a|⁻¹ mellin f (s / a)
theorem mellin_comp_mul_left {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] (f : E) (s : ) {a : } (ha : 0 < a) :
mellin (λ (t : ), f (a * t)) s = a ^ -s mellin f s
theorem mellin_comp_mul_right {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] (f : E) (s : ) {a : } (ha : 0 < a) :
mellin (λ (t : ), f (t * a)) s = a ^ -s mellin f s
theorem mellin_comp_inv {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] (f : E) (s : ) :
mellin (λ (t : ), f t⁻¹) s = mellin f (-s)
def has_mellin {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space 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} [normed_add_comm_group E] [normed_space E] [complete_space E] {f g : E} {s : } (hf : mellin_convergent f s) (hg : mellin_convergent g s) :
has_mellin (λ (t : ), f t + g t) s (mellin f s + mellin g s)
theorem has_mellin_sub {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {f g : E} {s : } (hf : mellin_convergent f s) (hg : mellin_convergent g s) :
has_mellin (λ (t : ), f t - g t) s (mellin f s - mellin g s)

Convergence of Mellin transform integrals #

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

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 +∞.

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 : } (hfc : measure_theory.locally_integrable_on f (set.Ioi 0) measure_theory.measure_space.volume) (hf_top : f =O[filter.at_top] λ (t : ), t ^ -a) (hs_top : s < a) (hf_bot : f =O[nhds_within 0 (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} [normed_add_comm_group E] [normed_space E] {a b : } {f : E} {s : } (hfc : measure_theory.locally_integrable_on f (set.Ioi 0) measure_theory.measure_space.volume) (hf_top : f =O[filter.at_top] λ (t : ), t ^ -a) (hs_top : s.re < a) (hf_bot : f =O[nhds_within 0 (set.Ioi 0)] λ (t : ), t ^ -b) (hs_bot : b < s.re) :
theorem is_O_rpow_top_log_smul {E : Type u_1} [normed_add_comm_group E] [normed_space E] {a b : } {f : E} (hab : b < a) (hf : f =O[filter.at_top] λ (t : ), t ^ -a) :
(λ (t : ), real.log 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} [normed_add_comm_group E] [normed_space E] {a b : } {f : E} (hab : a < b) (hf : f =O[nhds_within 0 (set.Ioi 0)] λ (t : ), t ^ -a) :
(λ (t : ), real.log t f t) =O[nhds_within 0 (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} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {f : E} {s : } (hfc : measure_theory.locally_integrable_on f (set.Ioi 0) measure_theory.measure_space.volume) (hf_top : f =O[filter.at_top] λ (t : ), t ^ -a) (hs_top : s.re < a) (hf_bot : f =O[nhds_within 0 (set.Ioi 0)] λ (t : ), t ^ -b) (hs_bot : b < s.re) :
mellin_convergent (λ (t : ), real.log t f t) s has_deriv_at (mellin f) (mellin (λ (t : ), real.log 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} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {f : E} {s : } (hfc : measure_theory.locally_integrable_on f (set.Ioi 0) measure_theory.measure_space.volume) (hf_top : f =O[filter.at_top] λ (t : ), t ^ -a) (hs_top : s.re < a) (hf_bot : f =O[nhds_within 0 (set.Ioi 0)] λ (t : ), t ^ -b) (hs_bot : b < s.re) :

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} [normed_add_comm_group E] [normed_space E] {a b : } (ha : 0 < a) {f : E} {s : } (hfc : measure_theory.locally_integrable_on f (set.Ioi 0) measure_theory.measure_space.volume) (hf_top : f =O[filter.at_top] λ (t : ), rexp (-a * t)) (hf_bot : f =O[nhds_within 0 (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} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } (ha : 0 < a) {f : E} {s : } (hfc : measure_theory.locally_integrable_on f (set.Ioi 0) measure_theory.measure_space.volume) (hf_top : f =O[filter.at_top] λ (t : ), rexp (-a * t)) (hf_bot : f =O[nhds_within 0 (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 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.