The Fourier transform of the two-sided exponential

For 0 < a the function x ↦ exp (-(a * |x|)) on ℝ is integrable, and pairing it against the oscillation exp (b * x * I) produces the Lorentzian 2 * a / (a ^ 2 + b ^ 2). In Mathlib's normalisation 𝓕 f ξ = ∫ x, exp (-2 π i x ξ) f x this reads

𝓕 (fun x ↦ exp (-(a * |x|))) ξ = 2 * a / (a ^ 2 + (2 * π * ξ) ^ 2).

The proof splits the line at the origin, where |x| becomes ∓x, and evaluates the two resulting complex exponential integrals with integral_exp_mul_complex_Iic and integral_exp_mul_complex_Ioi.

Main results

• TauCeti.integral_exp_mul_I_mul_exp_neg_mul_abs: the Lorentzian pairing;
• TauCeti.fourier_exp_neg_mul_abs: the Fourier transform itself.

theorem TauCeti.integral_exp_mul_I_mul_exp_neg_mul_abs {a : ℝ} (ha : 0 < a) (b : ℝ) : ∫ (x : ℝ), Complex.exp (↑b * ↑x * Complex.I) * ↑(Real.exp (-(a * |x|))) = ↑(2 * a / (a ^ 2 + b ^ 2))

The Lorentzian pairing of the two-sided exponential with a complex oscillation.

theorem TauCeti.fourier_exp_neg_mul_abs {a : ℝ} (ha : 0 < a) (ξ : ℝ) : FourierTransform.fourier (fun (x : ℝ) => ↑(Real.exp (-(a * |x|)))) ξ = ↑(2 * a / (a ^ 2 + (2 * Real.pi * ξ) ^ 2))

The Fourier transform of the two-sided exponential. With Mathlib's normalisation 𝓕 f ξ = ∫ x, exp (-2 π i x ξ) f x, the transform of x ↦ exp (-(a * |x|)) is the Lorentzian 2 * a / (a ^ 2 + (2 * π * ξ) ^ 2).