Jordan's integral bound

The estimate

$$\int_0^\pi e^{-c\sin\theta}\,d\theta \;\le\; \frac{\pi}{c} \qquad (c > 0)$$

which is the analytic engine of Jordan's lemma in contour integration. The integrand is close to 1 near the endpoints θ = 0, π, so the bound is not obtained by a pointwise estimate on the whole interval; what makes it work is Jordan's inequality sin θ ≥ (2/π) θ on [0, π/2] (Mathlib's Real.mul_le_sin), which forces enough decay near the endpoint to make the whole integral O(1/c).

Applied to |e^{iaz}| = e^{-aR\sin\theta} on an arc of radius R, the relevant instance is c = aR, giving the bound 1/(aR); its 1/R factor is what cancels the R in the arc length πR. That is why Jordan's lemma beats the naive ML bound, which would instead need the integrand itself to decay faster than 1/R.

Main results

• TauCeti.integral_exp_neg_mul_sin_le — the bound above.

References

• C. Jordan, Cours d'analyse de l'École Polytechnique, vol. 2 (1894), §270.
• P. Henrici, Applied and Computational Complex Analysis, vol. 1, §4.8.

theorem TauCeti.integral_exp_neg_mul_sin_le (c : ℝ) (hc : 0 < c) : ∫ (θ : ℝ) in 0..Real.pi, Real.exp (-c * Real.sin θ) ≤ Real.pi / c

Jordan's integral bound. For c > 0, ∫₀^π e^{-c sin θ} dθ ≤ π / c.