Negative powers as Gamma mixtures of exponentials

For -1 < α and 0 < x, Euler's integral gives x ^ (-(α + 1)) = Γ(α + 1)⁻¹ * ∫ s in Ioi 0, s ^ α * exp (-(x * s)). Substituting this into a power-weighted half-line integral and exchanging the two integrals turns it into a power-weighted integral of the Laplace transform of the integrand:

∫ x in Ioi 0, x ^ (-(α + 1)) • g x = Γ(α + 1)⁻¹ • ∫ s in Ioi 0, s ^ α • ∫ x in Ioi 0, exp (-(x * s)) • g x.

The only hypothesis is integrability of the left-hand integrand, which by Tonelli's theorem is exactly the absolute integrability needed for Fubini's theorem. This reduces singular power-law integrals, such as the compensated integrals against stable Lévy measures, to integrals of rational Laplace transforms. For the sine-compensated kernel exp (i t x) - 1 - i t sin x and its real counterpart exp (-a * x) - 1 + a * sin x, these Laplace transforms are computed explicitly.

The substitution t ↦ 1 / t turns Euler's integral into ∫ t in Ioi 0, t ^ (-(a + 1)) * exp (-(r / t)) = (1 / r) ^ a * Γ(a) for 0 < a and 0 < r, the normalization of the inverse-gamma density; averaging Gaussians exp (-π ‖z‖² / t) in the scale t against such powers produces the kernels ‖z‖ ^ (-2a) of the Riesz potentials and transforms.

Main results

• TauCeti.integrableOn_rpow_mul_exp_neg_mul_Ioi: the integrand of Euler's integral ∫ t in Ioi 0, t ^ (a - 1) * exp (-(r * t)) is integrable.
• TauCeti.integral_rpow_mul_exp_neg_div_Ioi, TauCeti.integrableOn_rpow_mul_exp_neg_div_Ioi: Euler's integral in the inverted variable.
• TauCeti.integrable_rpow_mul_exp_neg_mul_smul_prod: the joint integrand of the Gamma-mixture representation is integrable on the product of two half-lines, so Fubini's theorem applies.
• TauCeti.integrableOn_rpow_smul_integral_exp_neg_mul_smul: the power-weighted Laplace transform is integrable on the positive half-line.
• TauCeti.integral_Ioi_rpow_neg_smul: the exchange identity displayed above.
• TauCeti.integral_Ioi_exp_neg_mul_mul_sin: the Laplace transform 1 / (1 + s ^ 2) of sin on the positive half-line.
• TauCeti.integral_Ioi_exp_neg_mul_smul_cexp_sub_one_sub_sin: the Laplace transform (s - i t)⁻¹ - s⁻¹ - i t / (1 + s ^ 2) of the sine-compensated kernel.
• TauCeti.integral_Ioi_exp_neg_mul_mul_exp_sub_one_add_sin: the Laplace transform (s + a)⁻¹ - s⁻¹ + a / (1 + s ^ 2) of the real sine-compensated kernel.

theorem TauCeti.integrableOn_rpow_mul_exp_neg_mul_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (a - 1) * Real.exp (-(r * t))) (Set.Ioi 0) MeasureTheory.volume

The integrand t ^ (a - 1) exp (-r t) of Euler's integral is integrable on the positive half-line for 0 < a and 0 < r.

theorem TauCeti.integral_rpow_mul_exp_neg_div_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : ∫ (t : ℝ) in Set.Ioi 0, t ^ (-(a + 1)) * Real.exp (-(r / t)) = (1 / r) ^ a * Real.Gamma a

Euler's integral in the inverted variable: ∫₀^∞ t ^ (-(a + 1)) exp (-r / t) dt = (1 / r) ^ a Γ(a) for 0 < a and 0 < r, by the substitution t ↦ 1 / t in Real.integral_rpow_mul_exp_neg_mul_Ioi.

theorem TauCeti.integrableOn_rpow_mul_exp_neg_div_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (-(a + 1)) * Real.exp (-(r / t))) (Set.Ioi 0) MeasureTheory.volume

The integrand t ^ (-(a + 1)) exp (-r / t) of Euler's integral in the inverted variable is integrable on the positive half-line for 0 < a and 0 < r.

theorem TauCeti.integrable_rpow_mul_exp_neg_mul_smul_prod {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : ℝ} {g : ℝ → E} (hα : -1 < α) (hint : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ (-(α + 1)) • g x) (Set.Ioi 0) MeasureTheory.volume) : MeasureTheory.Integrable (Function.uncurry fun (x s : ℝ) => (s ^ α * Real.exp (-(x * s))) • g x) ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod (MeasureTheory.volume.restrict (Set.Ioi 0)))

The joint integrand (x, s) ↦ s ^ α exp (-x s) • g x of the Gamma-mixture representation is integrable on the product of two positive half-lines whenever x ↦ x ^ (-(α + 1)) • g x is integrable on the positive half-line.

theorem TauCeti.integrableOn_rpow_smul_integral_exp_neg_mul_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : ℝ} {g : ℝ → E} (hα : -1 < α) (hint : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ (-(α + 1)) • g x) (Set.Ioi 0) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (s : ℝ) => s ^ α • ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-(x * s)) • g x) (Set.Ioi 0) MeasureTheory.volume

The power-weighted Laplace transform s ↦ s ^ α • ∫ x in Ioi 0, exp (-(x * s)) • g x is integrable on the positive half-line whenever x ↦ x ^ (-(α + 1)) • g x is.

theorem TauCeti.integral_Ioi_rpow_neg_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : ℝ} {g : ℝ → E} [CompleteSpace E] (hα : -1 < α) (hint : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ (-(α + 1)) • g x) (Set.Ioi 0) MeasureTheory.volume) : ∫ (x : ℝ) in Set.Ioi 0, x ^ (-(α + 1)) • g x = (Real.Gamma (α + 1))⁻¹ • ∫ (s : ℝ) in Set.Ioi 0, s ^ α • ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-(x * s)) • g x

Negative powers as Gamma mixtures of exponentials. For -1 < α, a power-weighted half-line integral is a power-weighted integral of Laplace transforms: ∫ x in Ioi 0, x ^ (-(α + 1)) • g x = Γ(α + 1)⁻¹ • ∫ s in Ioi 0, s ^ α • ∫ x in Ioi 0, exp (-(x * s)) • g x.

theorem TauCeti.integral_Ioi_exp_neg_mul_mul_sin {s : ℝ} (hs : 0 < s) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-(x * s)) * Real.sin x = 1 / (1 + s ^ 2)

The Laplace transform of sine. For 0 < s, the Laplace transform of sin on the positive half-line is 1 / (1 + s ^ 2).

theorem TauCeti.integral_Ioi_exp_neg_mul_smul_cexp_sub_one_sub_sin {s : ℝ} (hs : 0 < s) (t : ℝ) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-(x * s)) • (Complex.exp (↑(t * x) * Complex.I) - 1 - ↑(t * Real.sin x) * Complex.I) = ↑(s / (s ^ 2 + t ^ 2) - s⁻¹) + ↑(t / (s ^ 2 + t ^ 2) - t / (1 + s ^ 2)) * Complex.I

The Laplace transform of the sine-compensated kernel. For 0 < s, the kernel x ↦ exp (i t x) - 1 - i t sin x has Laplace transform (s - i t)⁻¹ - s⁻¹ - i t / (1 + s ^ 2) on the positive half-line, written here through its real and imaginary parts.

theorem TauCeti.integral_Ioi_exp_neg_mul_mul_exp_sub_one_add_sin {s a : ℝ} (hs : 0 < s) (ha : 0 < s + a) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-(x * s)) * (Real.exp (-a * x) - 1 + a * Real.sin x) = (s + a)⁻¹ - s⁻¹ + a / (1 + s ^ 2)

The Laplace transform of the real sine-compensated exponential kernel, for 0 < s and 0 < s + a.