Jordan's lemma

A large semicircular arc contributes little to a contour integral whose integrand carries an oscillatory factor e^{iaz} with a > 0:

$$\left\|\int_{C_R} f(z)\,e^{iaz}\,dz\right\| \;\le\; \frac{\pi}{a}\,M_R, \qquad M_R = \sup_{C_R} \|f\|,$$

where C_R is the upper semicircle of radius R traversed counterclockwise.

The point is that the estimate needs no decay of f beyond boundedness, whereas the naive ML estimate ‖∫‖ ≤ (πR) · M_R would need M_R = o(1/R) even to stay bounded. Concluding that the arc contribution actually vanishes is a further step, and does require M_R → 0 — that is the hypothesis of tendsto_integral_semicircle_exp_mul_nhds_zero. The gain comes from |e^{iaz}| = e^{-aR\sin θ} on the arc together with TauCeti.integral_exp_neg_mul_sin_le, whose 1/(aR) cancels the arc length πR.

The estimate is sharp enough for the standard application: f z = z⁻¹ has M_R = 1/R → 0, so the arc term dies and the half-disc identity of WorkedExamples/HalfDisc/HalfResidue.lean survives the limit R → ∞. Note that without the oscillatory factor the arc term does not vanish at all — ∫ dz/z over the arc is iπ for every R — so the factor is essential, not a convenience.

Main results

• TauCeti.Contour.norm_integral_semicircle_exp_mul_le — Jordan's lemma as an explicit bound.
• TauCeti.Contour.tendsto_integral_semicircle_exp_mul_nhds_zero — the arc contribution tends to 0 along any radius filter on which the sup bound tends to 0.
• TauCeti.Contour.tendsto_integral_semicircle_exp_div_atTop_nhds_zero — the canonical instance f z = z⁻¹, where M_R = 1/R.

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.Contour.norm_integral_semicircle_exp_mul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a R M : ℝ} (ha : 0 < a) (hR : 0 ≤ R) (hM : ∀ θ ∈ Set.Icc 0 Real.pi, ‖f (circleMap 0 R θ)‖ ≤ M) : ‖∫ (θ : ℝ) in 0..Real.pi, (Complex.exp (Complex.I * ↑a * circleMap 0 R θ) * deriv (circleMap 0 R) θ) • f (circleMap 0 R θ)‖ ≤ Real.pi * M / a

Jordan's lemma. If ‖f‖ ≤ M on the upper semicircle of radius R, then for a > 0 the arc contribution of f z · e^{iaz} is at most π M / a in norm — a bound independent of R, obtained without assuming any decay of f.

No integrability hypothesis is imposed on the integrand, matching the Mathlib norm-of-integral idiom (intervalIntegral.norm_integral_le_of_norm_le constrains only the dominating function). When the parameterized integrand fails to be integrable the interval integral totalizes to 0 and the bound reads 0 ≤ π M / a, which holds since 0 ≤ M; the content of the lemma is therefore unchanged, and callers are not obliged to discharge integrability.

theorem TauCeti.Contour.tendsto_integral_semicircle_exp_mul_nhds_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℝ} {l : Filter ℝ} {M : ℝ → ℝ} (ha : 0 < a) (hpos : ∀ᶠ (R : ℝ) in l, 0 ≤ R) (hM : ∀ᶠ (R : ℝ) in l, ∀ θ ∈ Set.Icc 0 Real.pi, ‖f (circleMap 0 R θ)‖ ≤ M R) (hM0 : Filter.Tendsto M l (nhds 0)) : Filter.Tendsto (fun (R : ℝ) => ∫ (θ : ℝ) in 0..Real.pi, (Complex.exp (Complex.I * ↑a * circleMap 0 R θ) * deriv (circleMap 0 R) θ) • f (circleMap 0 R θ)) l (nhds 0)

The arc contribution vanishes. Along any filter of radii on which f admits a sup bound tending to 0 — the typical case M R = 1/R for f z = z⁻¹ — the semicircular arc integral of f z · e^{iaz} tends to 0. This is the form the improper-integral limit consumes.

As with the estimate it specialises, no integrability hypothesis is imposed; see norm_integral_semicircle_exp_mul_le for why the degenerate case is harmless.

theorem TauCeti.Contour.tendsto_integral_semicircle_exp_div_atTop_nhds_zero {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (R : ℝ) => ∫ (θ : ℝ) in 0..Real.pi, (Complex.exp (Complex.I * ↑a * circleMap 0 R θ) * deriv (circleMap 0 R) θ) • (circleMap 0 R θ)⁻¹) Filter.atTop (nhds 0)

The canonical instance of Jordan's lemma: the arc contribution of e^{iaz} / z vanishes as R → ∞. Here M_R = 1/R → 0, which is precisely the regime the naive ML bound cannot reach — it would give πR · (1/R) = π, a constant.