2` #

WorkedExamples/HalfDisc/Dirichlet.lean evaluates the Hungerbühler--Wasem motivating example in its complex form: the Cauchy principal values of e^{iaz}/z along the real segment [-R, R] converge to π i as R → ∞, the pole at the origin sitting on the contour and contributing only half its residue. This file cashes that in for the classical real statement it exists to prove — the Dirichlet integral

lim_{R → ∞} ∫_0^R sin (a x) / x dx = π / 2 for every frequency a > 0,

and in particular lim_{R → ∞} ∫_0^R sin x / x dx = π / 2. The limit is genuinely improper: x ↦ sin x / x is not Lebesgue integrable on [0, ∞), so there is no Bochner integral over Ioi 0 to state this about, and the result is a statement about the truncated integrals.

The bridge is a second, independent evaluation of the same principal value. Along the real axis the Dirichlet integrand splits as

e^{i a t} / t = cos (a t) / t + i · sin (a t) / t,

and the symmetric ε-excision at the origin treats the two parts completely differently:

the real part cos (a t) / t is odd, so each excised integral over [-R, R] vanishes identically — this is exactly why the principal value exists at all, the divergence of ∫ dt / t cancelling between the two sides;
the imaginary part sin (a t) / t is bounded (by |a|, since |sin u| ≤ |u|), so its excised integrals converge to the ordinary integral over [-R, R] by dominated convergence — no principal value is needed there.

So the principal value equals i · ∫_{-R}^{R} sin (a t) / t dt, and comparing with the half-disc evaluation of Dirichlet.lean through uniqueness of the principal value (HasCauchyPV.unique) turns the complex identity into a real one. Jordan's lemma disposes of the arc as R → ∞, and evenness of t ↦ sin (a t) / t halves the symmetric integral.

The frequency a is arbitrary in the principal-value identity — neither the cancellation nor the bound above needs anything of it — and only the passage to the limit R → ∞ requires a > 0, since that is where Jordan's lemma enters.

Main results #

TauCeti.Contour.hasCauchyPVAt_realSegment_dirichlet — the principal value of e^{iat}/t along [-R, R] is i · ∫_{-R}^{R} sin (a t) / t dt, for every frequency.
TauCeti.Contour.integral_sin_mul_div_neg_self_eq — comparing the two evaluations of that principal value: the symmetric integral is π minus the arc contribution.
TauCeti.Contour.tendsto_integral_sin_mul_div_neg_self_atTop — the symmetric integrals ∫_{-R}^{R} sin (a t) / t dt converge to π for a > 0.
TauCeti.Contour.tendsto_integral_sin_mul_div_atTop — the Dirichlet integral: ∫_0^R sin (a x) / x dx → π / 2 for a > 0.
TauCeti.Contour.tendsto_integral_sin_div_atTop and TauCeti.Contour.tendsto_integral_sinc_atTop — the unit-frequency case, in the sin x / x and the Real.sinc spellings.

References #

N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), Thm 3.3 and the improper-integral application motivating it.

The Dirichlet integrand along the real axis #

source

theorem TauCeti.Contour.dirichletIntegrand_ofReal (a t : ℝ) :

dirichletIntegrand a ↑t = ↑(Real.cos (a * t) / t) + ↑(Real.sin (a * t) / t) * Complex.I

The real and imaginary parts of the Dirichlet integrand along the real axis. For real t, e^{iat}/t = cos (a t)/t + i · sin (a t)/t. Both sides are 0 at t = 0 under the division-by-zero convention, so no hypothesis on t is needed.

Integrability of the excised real parts #

The two halves of the excised integral #

The principal value along the real segment, evaluated twice #

source

theorem TauCeti.Contour.hasCauchyPVAt_realSegment_dirichlet (a R : ℝ) :

HasCauchyPVAt (fun (t : ℝ) => ↑t) (-R) R (dirichletIntegrand a) 0 (↑(∫ (t : ℝ) in -R..R, Real.sin (a * t) / t) * Complex.I)

The principal value along the real segment, evaluated directly. For every frequency a and every real R, the Cauchy principal value of e^{iat}/t along [-R, R], excising the origin symmetrically, is i times the ordinary integral of sin (a t) / t.

Both defining clauses come from the split of the integrand into cos (a t)/t + i · sin (a t)/t: the excised real part integrates to 0 by oddness for every ε, while the imaginary part is bounded and its excised integrals converge by dominated convergence. Reversing a negative-radius interval negates both sides. No positivity of a is needed.

source

theorem TauCeti.Contour.integral_sin_mul_div_neg_self_eq {R : ℝ} (a : ℝ) (hR : 0 < R) :

↑(∫ (t : ℝ) in -R..R, Real.sin (a * t) / t) * Complex.I = ↑Real.pi * Complex.I - ∫ (θ : ℝ) in 0..Real.pi , dirichletIntegrand a (circleMap 0 R θ) * deriv (circleMap 0 R) θ

The two evaluations agree. Comparing the direct evaluation above with the half-disc evaluation of Dirichlet.lean through uniqueness of the principal value turns the complex identity into a real one: for each radius, i · ∫_{-R}^{R} sin (a t)/t dt is π i minus the arc contribution.

The improper integral #

source

theorem TauCeti.Contour.tendsto_integral_sin_mul_div_neg_self_atTop {a : ℝ} (ha : 0 < a) :

Filter.Tendsto (fun (R : ℝ) => ∫ (t : ℝ) in -R..R, Real.sin (a * t) / t) Filter.atTop (nhds Real.pi)

The symmetric Dirichlet integral. For a positive frequency the integrals over [-R, R] converge to π: Jordan's lemma kills the arc contribution of integral_sin_mul_div_neg_self_eq.

source

theorem TauCeti.Contour.tendsto_integral_sin_mul_div_atTop {a : ℝ} (ha : 0 < a) :

Filter.Tendsto (fun (R : ℝ) => ∫ (x : ℝ) in 0..R, Real.sin (a * x) / x) Filter.atTop (nhds (Real.pi / 2))

The Dirichlet integral, for an arbitrary positive frequency. ∫_0^R sin (a x) / x dx → π / 2 as R → ∞, for every a > 0 — the value is independent of the frequency. This is the Hungerbühler--Wasem motivating application: the pole of e^{iaz}/z sits on the contour of integration, so the classical residue theorem does not apply directly to this contour. The generalized theorem handles it without an indentation and weights the residue by the winding number ½ of a point on a smooth arc.

The limit is genuinely improper: x ↦ sin (a x) / x is not Lebesgue integrable on [0, ∞), so this is a statement about the truncated integrals and not about an integral over Ioi 0.

source

theorem TauCeti.Contour.tendsto_integral_sin_div_atTop :