An improper integral evaluated by the generalized residue theorem

The Hungerbühler–Wasem motivating example: the integrand e^{iaz} / z (a > 0) has a simple pole sitting on the contour, so the classical residue theorem does not apply, and the integral along the real axis exists only as a Cauchy principal value.

Running the half-disc contour of HalfDisc/Basic.lean and letting the radius grow:

• the half-residue theorem gives ∮ = π i · Res₀ f — half the enclosed-pole answer, because the generalized winding number at a smooth crossing is ½;
• hasCauchyPV_realSegment_diameter subtracts the arc and restates the result along the real line, leaving the segment alone;
• Jordan's lemma kills the arc as R → ∞, since ‖1/z‖ = 1/R → 0 on it.

The oscillatory factor is essential rather than cosmetic. At a = 0 the integrand is z⁻¹ and the arc integral equals i π for every R; it converges, but not to 0, so Jordan's lemma does not apply and the argument cannot deliver π i. The identity itself still holds there, and reading it off gives π i - i π = 0 — consistent with the symmetric principal values of 1/x all vanishing by oddness. Positive frequency is what forces the arc to zero, and the decay it supplies is exactly the regime the naive ML bound cannot reach.

Main results

• TauCeti.Contour.residue_dirichletIntegrand — Res₀ (e^{iaz}/z) = 1, for every frequency.
• TauCeti.Contour.neg_one_le_meromorphicOrderAt_dirichletIntegrand — the pole is at worst simple, the hypothesis the half-residue theorem consumes.
• TauCeti.Contour.hasCauchyPV_realSegment_dirichlet — for each radius, the principal value along [-R, R] on the real axis is π i minus the arc contribution.
• TauCeti.Contour.tendsto_integral_arc_dirichlet_atTop — the arc contribution vanishes, by Jordan's lemma for any positive frequency a > 0.
• TauCeti.Contour.tendsto_cauchyPV_realSegment_dirichlet — hence the principal values themselves, cauchyPV along [-R, R] on the real axis, converge to π i.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, Thm 3.3.

noncomputable def TauCeti.Contour.dirichletIntegrand (a : ℝ) (z : ℂ) : ℂ

The oscillatory Dirichlet integrand e^{iaz} / z, for a frequency a.

Equations

• TauCeti.Contour.dirichletIntegrand a z = Complex.exp (Complex.I * ↑a * z) / z

theorem TauCeti.Contour.dirichletIntegrand_eq (a : ℝ) (z : ℂ) : dirichletIntegrand a z = Complex.exp (Complex.I * ↑a * z) * z⁻¹

theorem TauCeti.Contour.meromorphicAt_dirichletIntegrand (a : ℝ) : MeromorphicAt (dirichletIntegrand a) 0

theorem TauCeti.Contour.residue_dirichletIntegrand (a : ℝ) : residue (dirichletIntegrand a) 0 = 1

The residue of e^{iaz}/z at the origin is 1, for every frequency.

theorem TauCeti.Contour.differentiableOn_dirichletIntegrand (a : ℝ) : DifferentiableOn ℂ (dirichletIntegrand a) (Set.univ \ {0})

The Dirichlet integrand is holomorphic away from the origin.

theorem TauCeti.Contour.neg_one_le_meromorphicOrderAt_dirichletIntegrand (a : ℝ) : ↑(-1) ≤ meromorphicOrderAt (dirichletIntegrand a) 0

The pole at the origin is at worst simple, for every frequency: the punctured limit of z · e^{iaz}/z exists, which is exactly the criterion of neg_one_le_meromorphicOrderAt_of_tendsto_sub_mul. This is the hypothesis the half-residue theorem consumes.

theorem TauCeti.Contour.hasCauchyPV_realSegment_dirichlet (a : ℝ) {R : ℝ} (hR : 0 < R) : HasCauchyPV (fun (t : ℝ) => ↑t) (-R) R (dirichletIntegrand a) (↑Real.pi * Complex.I - ∫ (θ : ℝ) in 0..Real.pi, dirichletIntegrand a (circleMap 0 R θ) * deriv (circleMap 0 R) θ)

The identity along the real segment. For each positive radius the principal value of e^{iaz}/z along [-R, R] on the real axis is π i minus the arc contribution. The pole sits on the path of integration, so this is a genuine principal value, not an ordinary integral.

theorem TauCeti.Contour.tendsto_integral_arc_dirichlet_atTop {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (R : ℝ) => ∫ (θ : ℝ) in 0..Real.pi, dirichletIntegrand a (circleMap 0 R θ) * deriv (circleMap 0 R) θ) Filter.atTop (nhds 0)

The arc contribution vanishes for a positive frequency. This is Jordan's lemma: on the semicircle the amplitude bound is ‖1/z‖ = 1/R → 0, which the naive ML bound could not exploit.

theorem TauCeti.Contour.tendsto_cauchyPV_realSegment_dirichlet {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (R : ℝ) => cauchyPV (fun (t : ℝ) => ↑t) (-R) R (dirichletIntegrand a)) Filter.atTop (nhds (↑Real.pi * Complex.I))

The improper principal value. As the radius grows, the Cauchy principal values of e^{iaz}/z along [-R, R] on the real axis converge to π i — the half-residue, evaluated by the Hungerbühler–Wasem theorem on a contour running through the pole, where the classical residue theorem does not apply.

This is the roadmap's improper-integral acceptance criterion: the statement is about cauchyPV along the real line, with no reference to the auxiliary half-disc contour used to prove it.