Regularized incomplete Mellin transforms

The regularized incomplete Mellin transform of a C^N integrand on a compact interval [0, a] continues holomorphically from {0 < re α} to {-(N : ℝ) < re α}. This is the one-variable engine for finite-order continuation of regularized Dirichlet integrals.

noncomputable def Complex.mellinSlope (a : ℝ) (K : ℝ → ℂ) (t : ℝ) : ℂ

The slope remainder (K t - K 0) / t, equal to the one-sided derivative at the origin.

Equations

• Complex.mellinSlope a K t = if t = 0 then derivWithin K (Set.Icc 0 a) 0 else slope K 0 t

theorem Complex.eq_add_mellinSlope {a : ℝ} {K : ℝ → ℂ} {t : ℝ} : K t = K 0 + ↑t * mellinSlope a K t

The first-order Taylor identity on [0, a].

theorem Complex.continuousOn_mellinSlope {a : ℝ} (ha : 0 < a) {K : ℝ → ℂ} (hK : ContDiffOn ℝ 1 K (Set.Icc 0 a)) : ContinuousOn (mellinSlope a K) (Set.Icc 0 a)

A C¹ integrand on [0, a] has a continuous slope remainder.

theorem Complex.integrableOn_cpow_Icc {α : ℂ} {a : ℝ} (hα : 0 < α.re) (ha : 0 ≤ a) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ↑t ^ (α - 1)) (Set.Icc 0 a) MeasureTheory.volume

Integrability of t ↦ (t : ℂ)^{α - 1} on [0, a] when 0 < re α.

theorem Complex.integrableOn_cpow_mul_Icc {α : ℂ} {a : ℝ} (hα : 0 < α.re) (ha : 0 ≤ a) {K : ℝ → ℂ} (hK : ContinuousOn K (Set.Icc 0 a)) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ↑t ^ (α - 1) * K t) (Set.Icc 0 a) MeasureTheory.volume

Integrability of a continuous integrand against the Mellin kernel on [0, a].

noncomputable def Complex.regIncompleteMellin (α : ℂ) (a : ℝ) (K : ℝ → ℂ) : ℂ

The regularized incomplete Mellin transform on [0, a].

Equations

• α.regIncompleteMellin a K = (Complex.Gamma α)⁻¹ * ∫ (t : ℝ) in Set.Icc 0 a, ↑t ^ (α - 1) * K t

theorem Complex.integral_Icc_cpow {β : ℂ} {a : ℝ} (hβ : 0 < β.re) (ha : 0 < a) : ∫ (t : ℝ) in Set.Icc 0 a, ↑t ^ (β - 1) = ↑a ^ β / β

The integral of t^{β-1} on [0, a] for 0 < re β.

theorem Complex.regIncompleteMellin_const {α : ℂ} {a : ℝ} (hα : 0 < α.re) (ha : 0 < a) (c : ℂ) : (α.regIncompleteMellin a fun (x : ℝ) => c) = c * ↑a ^ α * (Gamma (α + 1))⁻¹

Evaluating the Mellin transform of a constant.

theorem Complex.regIncompleteMellin_pow {α : ℂ} {a : ℝ} (hα : 0 < α.re) (ha : 0 < a) (k : ℕ) : (α.regIncompleteMellin a fun (t : ℝ) => ↑t ^ k) = ↑a ^ (α + ↑k) * Polynomial.eval α (ascPochhammer ℂ k) * (Gamma (α + ↑k + 1))⁻¹

Mellin transform of the monomial t ↦ t ^ k.

noncomputable def Complex.mellinPeanoRemainder (N : ℕ) (a : ℝ) (K : ℝ → ℂ) (t : ℝ) : ℂ

The Peano remainder of order N ≥ 1.

Equations

• Complex.mellinPeanoRemainder N a K t = if t = 0 then (↑N.factorial)⁻¹ * iteratedDerivWithin N K (Set.Icc 0 a) 0 else (t ^ N)⁻¹ • (K t - taylorWithinEval K (N - 1) (Set.Icc 0 a) 0 t)

theorem Complex.eq_taylor_add_mellinPeanoRemainder {N : ℕ} (hN : 0 < N) {a : ℝ} {K : ℝ → ℂ} {t : ℝ} (ht : t ∈ Set.Icc 0 a) : K t = taylorWithinEval K (N - 1) (Set.Icc 0 a) 0 t + t ^ N • mellinPeanoRemainder N a K t

theorem Complex.taylorWithinEval_succ_pred {N : ℕ} (hN : 0 < N) (K : ℝ → ℂ) (a x : ℝ) : taylorWithinEval K N (Set.Icc 0 a) 0 x = taylorWithinEval K (N - 1) (Set.Icc 0 a) 0 x + ((↑N.factorial)⁻¹ * x ^ N) • iteratedDerivWithin N K (Set.Icc 0 a) 0

theorem Complex.continuousOn_mellinPeanoRemainder {N : ℕ} (hN : 0 < N) {a : ℝ} (ha : 0 < a) {K : ℝ → ℂ} (hK : ContDiffOn ℝ (↑N) K (Set.Icc 0 a)) : ContinuousOn (mellinPeanoRemainder N a K) (Set.Icc 0 a)

The Peano remainder of a C^N integrand is continuous on [0, a].

theorem Complex.integral_Icc_eq_mellin_indicator {α : ℂ} {a : ℝ} {K : ℝ → ℂ} : ∫ (t : ℝ) in Set.Icc 0 a, ↑t ^ (α - 1) * K t = mellin ((Set.Ioc 0 a).indicator K) α

Extending a compactly supported integrand by zero, the incomplete Mellin integral agrees with Mathlib's Mellin transform.

theorem Complex.locallyIntegrableOn_indicator_Ioc {a : ℝ} {K : ℝ → ℂ} (hK : ContinuousOn K (Set.Icc 0 a)) : MeasureTheory.LocallyIntegrableOn ((Set.Ioc 0 a).indicator K) (Set.Ioi 0) MeasureTheory.volume

Zero extension of a continuous integrand on [0, a] is locally integrable on (0, ∞).

theorem Complex.isBigO_atTop_indicator_Ioc {a : ℝ} (K : ℝ → ℂ) (b : ℝ) : (Set.Ioc 0 a).indicator K =O[Filter.atTop] fun (t : ℝ) => t ^ (-b)

Compact support on [0, a] gives arbitrary polynomial decay at infinity.

theorem Complex.isBigO_nhdsGT_zero_indicator_Ioc {a : ℝ} {K : ℝ → ℂ} (hK : ContinuousOn K (Set.Icc 0 a)) : (Set.Ioc 0 a).indicator K =O[nhdsWithin 0 (Set.Ioi 0)] fun (t : ℝ) => t ^ (-0)

A continuous integrand on [0, a] is O(1) at the origin.

theorem Complex.analyticOn_regIncompleteMellin {a : ℝ} {K : ℝ → ℂ} (hK : ContinuousOn K (Set.Icc 0 a)) : AnalyticOn ℂ (fun (α : ℂ) => α.regIncompleteMellin a K) {α : ℂ | 0 < α.re}

The regularized incomplete Mellin transform of a continuous integrand is holomorphic on {0 < re α}.

theorem Complex.regIncompleteMellin_add {α : ℂ} {a : ℝ} (hα : 0 < α.re) (ha : 0 ≤ a) {K L : ℝ → ℂ} (hK : ContinuousOn K (Set.Icc 0 a)) (hL : ContinuousOn L (Set.Icc 0 a)) : (α.regIncompleteMellin a fun (t : ℝ) => K t + L t) = α.regIncompleteMellin a K + α.regIncompleteMellin a L

Linearity of the regularized incomplete Mellin transform in the integrand.

theorem Complex.regIncompleteMellin_const_mul {α : ℂ} {a : ℝ} {K : ℝ → ℂ} (c : ℂ) : (α.regIncompleteMellin a fun (t : ℝ) => c * K t) = c * α.regIncompleteMellin a K

theorem Complex.regIncompleteMellin_mul_pow {α : ℂ} {a : ℝ} {K : ℝ → ℂ} (k : ℕ) : (α.regIncompleteMellin a fun (t : ℝ) => ↑t ^ k * K t) = Polynomial.eval α (ascPochhammer ℂ k) * (α + ↑k).regIncompleteMellin a K

Mellin of t ↦ t^k K t is the Pochhammer shift of the Mellin of K.

theorem Complex.taylorWithinEval_eq_sum_cpow {n : ℕ} (K : ℝ → ℂ) (a t : ℝ) : taylorWithinEval K n (Set.Icc 0 a) 0 t = ∑ k ∈ Finset.range (n + 1), (↑k.factorial)⁻¹ * iteratedDerivWithin k K (Set.Icc 0 a) 0 * ↑t ^ k

The Taylor polynomial of order n as a sum of monomials.

theorem Complex.regIncompleteMellin_eq_taylor_peano {N : ℕ} (hN : 0 < N) {a : ℝ} (ha : 0 < a) {K : ℝ → ℂ} (hK : ContDiffOn ℝ (↑N) K (Set.Icc 0 a)) {α : ℂ} (hα : 0 < α.re) : α.regIncompleteMellin a K = ∑ k ∈ Finset.range N, (↑k.factorial)⁻¹ * iteratedDerivWithin k K (Set.Icc 0 a) 0 * (↑a ^ (α + ↑k) * Polynomial.eval α (ascPochhammer ℂ k) * (Gamma (α + ↑k + 1))⁻¹) + Polynomial.eval α (ascPochhammer ℂ N) * (α + ↑N).regIncompleteMellin a (mellinPeanoRemainder N a K)

Native identity: the incomplete Mellin of a C^N integrand is the explicit Mellin of its Taylor polynomial plus a Pochhammer-shifted Mellin of the Peano remainder.

theorem Complex.exists_regIncompleteMellin_continuation {N : ℕ} {a : ℝ} (ha : 0 < a) {K : ℝ → ℂ} (hK : ContDiffOn ℝ (↑N) K (Set.Icc 0 a)) : ∃ (Φ : ℂ → ℂ), AnalyticOn ℂ Φ {α : ℂ | -↑N < α.re} ∧ Set.EqOn Φ (fun (α : ℂ) => α.regIncompleteMellin a K) {α : ℂ | 0 < α.re}

Finite differentiability of the integrand yields an analytic continuation of the regularized incomplete Mellin transform from {0 < re α} to {-(N : ℝ) < re α}.