Truncated Laplace transforms of bounded functions

For f : ℝ → ℂ, this file studies the Laplace transform G z = ∫ t in Ici 0, f t * exp (-z t) and its truncations G_T z = ∫ t in 0..T, f t * exp (-z t):

• each truncation is entire (differentiable_intervalIntegral_mul_cexp_neg_mul), and, for f bounded on [0, ∞), the full transform is holomorphic on 0 < re z (differentiableOn_integral_mul_cexp_neg_mul), being a locally uniform limit of truncations;
• if ‖f‖ ≤ M on [0, ∞), the tail bound ‖G z - G_T z‖ ≤ M exp (-T re z) / re z holds for 0 < re z (norm_integral_sub_intervalIntegral_mul_cexp_neg_mul_le), and if ‖f‖ ≤ M on [0, T], then ‖G_T z‖ ≤ M exp (-T re z) / (-re z) for re z < 0 (norm_intervalIntegral_mul_cexp_neg_mul_le_of_re_neg).

The substitution x = exp t identifies ∫ x in u..v, x ^ (-z - 1) with the truncated Laplace transform ∫ t in log u..log v, exp (-z t) of the constant function 1 (intervalIntegral_ofReal_cpow_neg_sub_one); this links Dirichlet series, via integrals against x ^ (-z - 1), to Laplace transforms of step functions t ↦ a ⌊exp t⌋₊.

These are the analytic inputs of Newman's contour argument for his Tauberian theorem.

theorem TauCeti.intervalIntegrable_mul_cexp_neg_mul_iff {f : ℝ → ℂ} {a b : ℝ} (z : ℂ) : IntervalIntegrable (fun (t : ℝ) => f t * Complex.exp (-z * ↑t)) MeasureTheory.volume a b ↔ IntervalIntegrable f MeasureTheory.volume a b

Multiplying by the exponential kernel cexp (-z t) does not change interval integrability.

theorem TauCeti.aestronglyMeasurable_mul_cexp_neg_mul_iff {f : ℝ → ℂ} {μ : MeasureTheory.Measure ℝ} (z : ℂ) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => f t * Complex.exp (-z * ↑t)) μ ↔ MeasureTheory.AEStronglyMeasurable f μ

Multiplying by the exponential kernel cexp (-z t) does not change almost-everywhere strong measurability.

theorem TauCeti.differentiable_intervalIntegral_mul_cexp_neg_mul {f : ℝ → ℂ} {a b : ℝ} : Differentiable ℂ fun (z : ℂ) => ∫ (t : ℝ) in a..b, f t * Complex.exp (-z * ↑t)

Truncated Laplace transforms are entire. The function z ↦ ∫ t in a..b, f t * exp (-z t) is complex differentiable everywhere. If f is not interval integrable on [a, b], it is identically 0.

theorem TauCeti.intervalIntegral_ofReal_cpow_neg_sub_one {u v : ℝ} (hu : 0 < u) (hv : 0 < v) (z : ℂ) : ∫ (x : ℝ) in u..v, ↑x ^ (-z - 1) = ∫ (t : ℝ) in Real.log u..Real.log v, Complex.exp (-z * ↑t)

Substitution x = exp t. For 0 < u and 0 < v, the integral of x ^ (-z - 1) over [u, v] is the truncated Laplace transform ∫ t in log u..log v, exp (-z t) of the constant function 1.

theorem TauCeti.norm_mul_cexp_neg_mul_le {M : ℝ} {w z : ℂ} {t : ℝ} (h : ‖w‖ ≤ M) : ‖w * Complex.exp (-z * ↑t)‖ ≤ M * Real.exp (-z.re * t)

Pointwise bound on the Laplace integrand: if ‖w‖ ≤ M, then ‖w * exp (-z t)‖ ≤ M * exp (-re z * t) for real t.

theorem TauCeti.integrableOn_mul_cexp_neg_mul {f : ℝ → ℂ} {M : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0))) (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) {z : ℂ} (hz : 0 < z.re) : MeasureTheory.IntegrableOn (fun (t : ℝ) => f t * Complex.exp (-z * ↑t)) (Set.Ici 0) MeasureTheory.volume

For 0 < re z, the Laplace integrand of a function bounded on [0, ∞) is integrable there.

theorem TauCeti.norm_integral_sub_intervalIntegral_mul_cexp_neg_mul_le {f : ℝ → ℂ} {M T : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0))) (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) {z : ℂ} (hz : 0 < z.re) (hT : 0 ≤ T) : ‖(∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t)) - ∫ (t : ℝ) in 0..T, f t * Complex.exp (-z * ↑t)‖ ≤ M * Real.exp (-z.re * T) / z.re

Tail bound. For 0 < re z and 0 ≤ T, the Laplace transform of a function bounded by M on [0, ∞) differs from its truncation at T by at most M exp (-T re z) / re z.

theorem TauCeti.norm_intervalIntegral_mul_cexp_neg_mul_le_of_re_neg {f : ℝ → ℂ} {M T : ℝ} (hbound : ∀ t ∈ Set.Icc 0 T, ‖f t‖ ≤ M) {z : ℂ} (hz : z.re < 0) (hT : 0 ≤ T) : ‖∫ (t : ℝ) in 0..T, f t * Complex.exp (-z * ↑t)‖ ≤ M * Real.exp (-z.re * T) / -z.re

Left half-plane bound. For re z < 0 and 0 ≤ T, the truncated Laplace transform of a function bounded by M on [0, T] is at most M exp (-T re z) / (-re z).

theorem TauCeti.differentiableOn_integral_mul_cexp_neg_mul {f : ℝ → ℂ} {M : ℝ} (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) : DifferentiableOn ℂ (fun (z : ℂ) => ∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t)) {z : ℂ | 0 < z.re}

Holomorphy of the Laplace transform. If f is bounded on [0, ∞), its Laplace transform z ↦ ∫ t in Ici 0, f t * exp (-z t) is complex differentiable on the half-plane 0 < re z.