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 #

source
theorem complex.cpow_mul_of_real_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (z : ℂ) :
↑x ^ (↑y * z) = ↑(x ^ y) ^ z
source
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
source
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
source
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)
source
theorem mellin_convergent.div_const {f : ℝ → ℂ} {s : ℂ} (hf : mellin_convergent f s) (a : ℂ) :
mellin_convergent (λ (t : ℝ), f t / a) s
source
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
source
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)
source
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
source
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)
source
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
source
theorem mellin_div_const (f : ℝ → ℂ) (s a : ℂ) :
mellin (λ (t : ℝ), f t / a) s = mellin f s / a
source
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)
source
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
source
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
source
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)
source
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
source
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)
source
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 #

source
theorem mellin_convergent_iff_norm {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℝ → E} {T : set ℝ} (hT : T ⊆ set.Ioi 0) (hT' : measurable_set T) (hfc : measure_theory.ae_strongly_measurable f (measure_theory.measure_space.volume.restrict (set.Ioi 0))) {s : ℂ} :
measure_theory.integrable_on (λ (t : ℝ), ↑t ^ (s - 1) • f t) T measure_theory.measure_space.volume ↔ measure_theory.integrable_on (λ (t : ℝ), t ^ (s.re - 1) * ‖f t‖) T measure_theory.measure_space.volume

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

source
theorem mellin_convergent_top_of_is_O {f : ℝ → ℝ} (hfc : measure_theory.ae_strongly_measurable f (measure_theory.measure_space.volume.restrict (set.Ioi 0))) {a s : ℝ} (hf : f =O[filter.at_top] λ (t : ℝ), t ^ -a) (hs : s < a) :
∃ (c : ℝ), 0 < c ∧ measure_theory.integrable_on (λ (t : ℝ), t ^ (s - 1) * f t) (set.Ioi c) measure_theory.measure_space.volume

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

source
theorem mellin_convergent_zero_of_is_O {b : ℝ} {f : ℝ → ℝ} (hfc : measure_theory.ae_strongly_measurable f (measure_theory.measure_space.volume.restrict (set.Ioi 0))) (hf : f =O[nhds_within 0 (set.Ioi 0)] λ (t : ℝ), t ^ -b) {s : ℝ} (hs : b < s) :
∃ (c : ℝ), 0 < c ∧ measure_theory.integrable_on (λ (t : ℝ), t ^ (s - 1) * f t) (set.Ioc 0 c) measure_theory.measure_space.volume

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.

source
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) :
measure_theory.integrable_on (λ (t : ℝ), t ^ (s - 1) * f t) (set.Ioi 0) measure_theory.measure_space.volume

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.

source
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) :
mellin_convergent f s
source
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.

source
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.

source
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.

source
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) :
differentiable_at ℂ (mellin f) 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.

source
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) :
mellin_convergent f s

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.

source
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) :
differentiable_at ℂ (mellin f) 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 #

source
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.

source
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.