The Laplace transform of |sin|

For 0 < a the rectified sine |sin t| has the Laplace transform

∫_{t > 0} |sin t| e^{-a t} dt = (1 + e^{-π a}) / ((1 - e^{-π a}) (1 + a²)),

and, since |sin| is even, the two-sided transform ∫_ℝ |sin t| e^{-a |t|} dt is twice that. One arch contributes ∫_0^π sin t e^{-a t} dt = (1 + e^{-π a}) / (1 + a²), and since |sin| is π-periodic every later arch contributes the same amount damped by a further factor e^{-π a}; summing the geometric series gives the closed form.

Main declarations

• TauCeti.integral_sin_mul_exp_neg_mul_zero_pi: the integral over one arch;
• TauCeti.integral_abs_sin_mul_exp_neg_mul_Ioi: the one-sided Laplace transform of |sin|;
• TauCeti.integral_abs_sin_mul_exp_neg_mul_abs: the two-sided transform ∫_ℝ |sin t| e^{-a |t|} dt = 2 (1 + e^{-π a}) / ((1 - e^{-π a}) (1 + a²)).

theorem TauCeti.integral_sin_mul_exp_neg_mul_zero_pi (a : ℝ) : ∫ (t : ℝ) in 0..Real.pi, Real.sin t * Real.exp (-(a * t)) = (1 + Real.exp (-(Real.pi * a))) / (1 + a ^ 2)

The Laplace integral of sin over one arch. For every real a, ∫_0^π sin t e^{-a t} dt = (1 + e^{-π a}) / (1 + a²).

theorem TauCeti.integrableOn_abs_sin_mul_exp_neg_mul_Ioi {a : ℝ} (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (t : ℝ) => |Real.sin t| * Real.exp (-(a * t))) (Set.Ioi 0) MeasureTheory.volume

For 0 < a, the function t ↦ |sin t| e^{-a t} is integrable on (0, ∞): it is dominated by e^{-a t}.

theorem TauCeti.integral_abs_sin_mul_exp_neg_mul_Ioi {a : ℝ} (ha : 0 < a) : ∫ (t : ℝ) in Set.Ioi 0, |Real.sin t| * Real.exp (-(a * t)) = (1 + Real.exp (-(Real.pi * a))) / ((1 - Real.exp (-(Real.pi * a))) * (1 + a ^ 2))

The Laplace transform of |sin|. For 0 < a, ∫_{t > 0} |sin t| e^{-a t} dt = (1 + e^{-π a}) / ((1 - e^{-π a}) (1 + a²)).

theorem TauCeti.integrable_abs_sin_mul_exp_neg_mul_abs {a : ℝ} (ha : 0 < a) : MeasureTheory.Integrable (fun (t : ℝ) => |Real.sin t| * Real.exp (-(a * |t|))) MeasureTheory.volume

For 0 < a, the function t ↦ |sin t| e^{-a |t|} is integrable on ℝ: it is dominated by e^{-a |t|}.

theorem TauCeti.integral_abs_sin_mul_exp_neg_mul_abs {a : ℝ} (ha : 0 < a) : ∫ (t : ℝ), |Real.sin t| * Real.exp (-(a * |t|)) = 2 * (1 + Real.exp (-(Real.pi * a))) / ((1 - Real.exp (-(Real.pi * a))) * (1 + a ^ 2))

The two-sided Laplace transform of |sin|. For 0 < a, ∫_ℝ |sin t| e^{-a |t|} dt = 2 (1 + e^{-π a}) / ((1 - e^{-π a}) (1 + a²)).