Residue theorem for rectangular contours

This file proves the residue theorem for rectangular contours. Mathlib already has Cauchy–Goursat for rectangles (Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable) and the Cauchy integral formula for circles. This file fills the gap between them by proving the residue formula for rectangular boundary integrals, together with a rotated principal log branch needed to evaluate the left-edge integral that crosses the standard cut.

The development proceeds in five stages:

• a notation Complex.boundaryIntegral for the oriented boundary integral over [z, w], with a Cauchy–Goursat wrapper and additivity/scaling lemmas;
• a rotated principal logarithm Complex.logNeg z := log (-z) + I·π with cut on the positive real axis, plus its derivative and corner-comparison identities with the standard Complex.log;
• explicit FTC-based evaluations of the four edge integrals of (s − ρ)⁻¹;
• a closed-form residue boundary integral ∮_{∂[z,w]} (s − ρ)⁻¹ ds = 2πi for ρ strictly inside the rectangle;
• a parametric residue theorem for sums of simple poles plus a holomorphic remainder, packaged as Complex.RectangleResidueData.

Main results

• Complex.hasDerivAt_log_neg: Complex.logNeg has derivative z⁻¹ on the rotated slit plane {z | -z ∈ slitPlane}.
• Complex.boundaryIntegral_inv_sub_eq_two_pi_I: for ρ strictly inside the rectangle [z, w], the boundary integral of (s − ρ)⁻¹ equals 2πi.
• Complex.boundaryIntegral_eq_residue_sum: for a Complex.RectangleResidueData bundle describing simple poles inside the rectangle plus a holomorphic remainder, the boundary integral equals 2πi times the sum of residues.
• Complex.boundaryIntegral_single_pole: the one-pole specialization.

References

• L. Ahlfors, Complex Analysis (3rd ed.), §4.5.
• E. Stein, R. Shakarchi, Complex Analysis, Ch. 2 §3 Theorem 3.1.
• W. Rudin, Real and Complex Analysis (3rd ed.), §10.42.

Tags

complex analysis, residue theorem, contour integral, Cauchy formula, rectangular contour

Boundary integral over a rectangle

noncomputable def Zeta32.Analytic.Contour.boundaryIntegral (f : ℂ → ℂ) (z w : ℂ) : ℂ

The oriented boundary integral of f over the rectangle [z, w], in the sign convention of Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable.

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta32.Analytic.Contour.boundaryIntegral_eq_zero_of_diffOn {f : ℂ → ℂ} {z w : ℂ} {s : Set ℂ} (hs : s.Countable) (hc : ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (hd : ∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ s, DifferentiableAt ℂ f x) : boundaryIntegral f z w = 0

Cauchy–Goursat for the boundary-integral notation: a function continuous on the closed rectangle and differentiable off a countable subset of the open rectangle has vanishing boundary integral.

Linearity of the boundary integral

theorem Zeta32.Analytic.Contour.boundaryIntegral_add (f g : ℂ → ℂ) (z w : ℂ) (hfb : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑z.im * Complex.I)) MeasureTheory.volume z.re w.re) (hgb : IntervalIntegrable (fun (x : ℝ) => g (↑x + ↑z.im * Complex.I)) MeasureTheory.volume z.re w.re) (hft : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑w.im * Complex.I)) MeasureTheory.volume z.re w.re) (hgt : IntervalIntegrable (fun (x : ℝ) => g (↑x + ↑w.im * Complex.I)) MeasureTheory.volume z.re w.re) (hfr : IntervalIntegrable (fun (y : ℝ) => f (↑w.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im) (hgr : IntervalIntegrable (fun (y : ℝ) => g (↑w.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im) (hfl : IntervalIntegrable (fun (y : ℝ) => f (↑z.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im) (hgl : IntervalIntegrable (fun (y : ℝ) => g (↑z.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im) : boundaryIntegral (fun (s : ℂ) => f s + g s) z w = boundaryIntegral f z w + boundaryIntegral g z w

The boundary integral is additive in the integrand.

theorem Zeta32.Analytic.Contour.boundaryIntegral_const_mul (k : ℂ) (f : ℂ → ℂ) (z w : ℂ) : boundaryIntegral (fun (s : ℂ) => k * f s) z w = k * boundaryIntegral f z w

The boundary integral pulls a complex constant outside.

Finite-sum decomposition

theorem Zeta32.Analytic.Contour.boundaryIntegral_finset_sum {ι : Type u_1} (S : Finset ι) (f : ι → ℂ → ℂ) (z w : ℂ) (hfb : ∀ i ∈ S, IntervalIntegrable (fun (x : ℝ) => f i (↑x + ↑z.im * Complex.I)) MeasureTheory.volume z.re w.re) (hft : ∀ i ∈ S, IntervalIntegrable (fun (x : ℝ) => f i (↑x + ↑w.im * Complex.I)) MeasureTheory.volume z.re w.re) (hfr : ∀ i ∈ S, IntervalIntegrable (fun (y : ℝ) => f i (↑w.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im) (hfl : ∀ i ∈ S, IntervalIntegrable (fun (y : ℝ) => f i (↑z.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im) : boundaryIntegral (fun (s : ℂ) => ∑ i ∈ S, f i s) z w = ∑ i ∈ S, boundaryIntegral (f i) z w

The boundary integral distributes over a finite sum of integrands.

Rotated principal logarithm logNeg

The standard branch Complex.log has its branch cut on the negative real axis. To evaluate boundary integrals on rectangles whose left edge crosses that cut, we introduce the rotated branch logNeg z := log (-z) + I·π, whose cut is on the positive real axis.

noncomputable def Zeta32.Analytic.Contour.logNeg (z : ℂ) : ℂ

A principal logarithm with branch cut on the positive real axis.

Equations

• Zeta32.Analytic.Contour.logNeg z = Complex.log (-z) + Complex.I * ↑Real.pi

theorem Zeta32.Analytic.Contour.hasDerivAt_log_neg {z : ℂ} (hz : -z ∈ Complex.slitPlane) : HasDerivAt logNeg z⁻¹ z

logNeg has derivative z⁻¹ whenever -z lies in the standard slit plane.

theorem Zeta32.Analytic.Contour.hasDerivAt_clog_neg_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : HasDerivAt f f' x) (h₂ : -f x ∈ Complex.slitPlane) : HasDerivAt (fun (t : ℝ) => logNeg (f t)) (f' / f x) x

Real-FTC chain rule for logNeg: if f : ℝ → ℂ has derivative f' at x and -(f x) lies in the standard slit plane, then t ↦ logNeg (f t) has derivative f' / f x at x.

theorem Zeta32.Analytic.Contour.log_neg_eq_log_of_im_pos {ζ : ℂ} (him : 0 < ζ.im) : logNeg ζ = Complex.log ζ

For points with positive imaginary part, logNeg agrees with Complex.log.

theorem Zeta32.Analytic.Contour.log_neg_eq_log_add_two_pi_I_of_im_neg {ζ : ℂ} (him : ζ.im < 0) : logNeg ζ = Complex.log ζ + 2 * ↑Real.pi * Complex.I

For points with negative imaginary part, logNeg differs from Complex.log by 2πi.

Edge integrals for (s − ρ)⁻¹

theorem Zeta32.Analytic.Contour.bottomEdge_integral_eq {z w ρ : ℂ} (hρ_im_lt : z.im < ρ.im) : ∫ (x : ℝ) in z.re..w.re, (↑x + ↑z.im * Complex.I - ρ)⁻¹ = Complex.log (↑w.re + ↑z.im * Complex.I - ρ) - Complex.log (↑z.re + ↑z.im * Complex.I - ρ)

Bottom-edge integral of (s − ρ)⁻¹ evaluated via FTC + standard log.

theorem Zeta32.Analytic.Contour.topEdge_integral_eq {z w ρ : ℂ} (hρ_im_lt : ρ.im < w.im) : ∫ (x : ℝ) in z.re..w.re, (↑x + ↑w.im * Complex.I - ρ)⁻¹ = Complex.log (↑w.re + ↑w.im * Complex.I - ρ) - Complex.log (↑z.re + ↑w.im * Complex.I - ρ)

Top-edge integral of (s − ρ)⁻¹ evaluated via FTC + standard log.

theorem Zeta32.Analytic.Contour.rightEdge_integral_eq {z w ρ : ℂ} (hρ_re_lt : ρ.re < w.re) : ∫ (y : ℝ) in z.im..w.im, (↑w.re + ↑y * Complex.I - ρ)⁻¹ = -Complex.I * (Complex.log (↑w.re + ↑w.im * Complex.I - ρ) - Complex.log (↑w.re + ↑z.im * Complex.I - ρ))

Right-edge integral of (s − ρ)⁻¹ evaluated via FTC + standard log.

theorem Zeta32.Analytic.Contour.leftEdge_integral_eq {z w ρ : ℂ} (hρ_re_lt : z.re < ρ.re) : ∫ (y : ℝ) in z.im..w.im, (↑z.re + ↑y * Complex.I - ρ)⁻¹ = -Complex.I * (logNeg (↑z.re + ↑w.im * Complex.I - ρ) - logNeg (↑z.re + ↑z.im * Complex.I - ρ))

Left-edge integral of (s − ρ)⁻¹ evaluated via FTC + the rotated logNeg branch. The left edge crosses the standard cut, so the standard Complex.log antiderivative does not work directly; logNeg (cut on the positive real axis) is the right branch here.

Closed-form principal-part rectangle integral

theorem Zeta32.Analytic.Contour.boundaryIntegral_inv_sub_eq_two_pi_I {z w ρ : ℂ} (hρ_re : ρ.re ∈ Set.Ioo z.re w.re) (hρ_im : ρ.im ∈ Set.Ioo z.im w.im) : boundaryIntegral (fun (s : ℂ) => (s - ρ)⁻¹) z w = 2 * ↑Real.pi * Complex.I

Cauchy integral formula on a rectangle. For ρ strictly inside the rectangle [z, w], the boundary integral of (s − ρ)⁻¹ equals 2πi.

This is the rectangular analogue of Mathlib's circle-based Cauchy integral formula for (s − ρ)⁻¹. The proof evaluates each of the four edge integrals using the FTC with the standard logarithm (three edges) and the rotated branch logNeg for the left edge, then verifies that the corner identity reduces to 2πi.

Parametric residue theorem

structure Zeta32.Analytic.Contour.RectangleResidueData (z w : ℂ) : Type

Hypothesis bundle for the parametric residue theorem on a rectangle.

The integrand decomposes as f s = ∑_{ρ ∈ S} c ρ · (s − ρ)⁻¹ + h s, where S is the finite set of simple poles (assumed inside the open rectangle), c ρ is the residue at each pole, and h is holomorphic on the closed rectangle off a countable set. The bundle records the integrability hypotheses needed to apply linearity of the boundary integral.

• S : Finset ℂ

  Finite set of distinct simple-pole locations inside the open rectangle.

• c : ℂ → ℂ

  Residue at each pole.

• h : ℂ → ℂ

  Holomorphic remainder.

• principalPart_int (ρ : ℂ) : ρ ∈ self.S → boundaryIntegral (fun (s : ℂ) => (s - ρ)⁻¹) z w = 2 * ↑Real.pi * Complex.I

  The principal-part rectangle integral evaluates to 2πi for each pole.

• h_continuousOn : ContinuousOn self.h (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)

  h is continuous on the closed rectangle.

• differentiabilityExceptions : Set ℂ

  Countable set off which h is differentiable on the open rectangle.

• h_off_countable : self.differentiabilityExceptions.Countable

  The off-set is countable.

• h_differentiableAt (x : ℂ) : x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ self.differentiabilityExceptions → DifferentiableAt ℂ self.h x

  h is differentiable on the open rectangle minus the off-set.

• pp_int_b (ρ : ℂ) : ρ ∈ self.S → IntervalIntegrable (fun (x : ℝ) => (↑x + ↑z.im * Complex.I - ρ)⁻¹) MeasureTheory.volume z.re w.re

  Principal-part bottom-edge integrability.

• pp_int_t (ρ : ℂ) : ρ ∈ self.S → IntervalIntegrable (fun (x : ℝ) => (↑x + ↑w.im * Complex.I - ρ)⁻¹) MeasureTheory.volume z.re w.re

  Principal-part top-edge integrability.

• pp_int_r (ρ : ℂ) : ρ ∈ self.S → IntervalIntegrable (fun (y : ℝ) => (↑w.re + ↑y * Complex.I - ρ)⁻¹) MeasureTheory.volume z.im w.im

  Principal-part right-edge integrability.

• pp_int_l (ρ : ℂ) : ρ ∈ self.S → IntervalIntegrable (fun (y : ℝ) => (↑z.re + ↑y * Complex.I - ρ)⁻¹) MeasureTheory.volume z.im w.im

  Principal-part left-edge integrability.

• h_int_b : IntervalIntegrable (fun (x : ℝ) => self.h (↑x + ↑z.im * Complex.I)) MeasureTheory.volume z.re w.re

  Remainder bottom-edge integrability.

• h_int_t : IntervalIntegrable (fun (x : ℝ) => self.h (↑x + ↑w.im * Complex.I)) MeasureTheory.volume z.re w.re

  Remainder top-edge integrability.

• h_int_r : IntervalIntegrable (fun (y : ℝ) => self.h (↑w.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im

  Remainder right-edge integrability.

• h_int_l : IntervalIntegrable (fun (y : ℝ) => self.h (↑z.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im

  Remainder left-edge integrability.

noncomputable def Zeta32.Analytic.Contour.RectangleResidueData.toIntegrand {z w : ℂ} (D : RectangleResidueData z w) (s : ℂ) : ℂ

The integrand assembled from a RectangleResidueData bundle: f s = ∑_{ρ ∈ S} c ρ · (s − ρ)⁻¹ + h s.

Equations

• D.toIntegrand s = ∑ ρ ∈ D.S, D.c ρ * (s - ρ)⁻¹ + D.h s

theorem Zeta32.Analytic.Contour.boundaryIntegral_eq_residue_sum {z w : ℂ} (D : RectangleResidueData z w) : boundaryIntegral D.toIntegrand z w = 2 * ↑Real.pi * Complex.I * ∑ ρ ∈ D.S, D.c ρ

Parametric residue theorem for rectangles.

If the integrand decomposes as f s = ∑_{ρ ∈ S} c ρ · (s − ρ)⁻¹ + h s per the hypotheses bundled in RectangleResidueData, then the boundary integral equals 2πi · ∑_{ρ ∈ S} c ρ. The proof combines linearity of the boundary integral, Cauchy–Goursat for the holomorphic remainder, and the principal-part value at each pole.

theorem Zeta32.Analytic.Contour.boundaryIntegral_single_pole {z w ρ c : ℂ} {h : ℂ → ℂ} (hpp : boundaryIntegral (fun (s : ℂ) => (s - ρ)⁻¹) z w = 2 * ↑Real.pi * Complex.I) (hh_cont : ContinuousOn h (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (hh_off : Set ℂ) (hh_off_c : hh_off.Countable) (hh_diff : ∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ hh_off, DifferentiableAt ℂ h x) (pp_b : IntervalIntegrable (fun (x : ℝ) => (↑x + ↑z.im * Complex.I - ρ)⁻¹) MeasureTheory.volume z.re w.re) (pp_t : IntervalIntegrable (fun (x : ℝ) => (↑x + ↑w.im * Complex.I - ρ)⁻¹) MeasureTheory.volume z.re w.re) (pp_r : IntervalIntegrable (fun (y : ℝ) => (↑w.re + ↑y * Complex.I - ρ)⁻¹) MeasureTheory.volume z.im w.im) (pp_l : IntervalIntegrable (fun (y : ℝ) => (↑z.re + ↑y * Complex.I - ρ)⁻¹) MeasureTheory.volume z.im w.im) (h_int_b : IntervalIntegrable (fun (x : ℝ) => h (↑x + ↑z.im * Complex.I)) MeasureTheory.volume z.re w.re) (h_int_t : IntervalIntegrable (fun (x : ℝ) => h (↑x + ↑w.im * Complex.I)) MeasureTheory.volume z.re w.re) (h_int_r : IntervalIntegrable (fun (y : ℝ) => h (↑w.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im) (h_int_l : IntervalIntegrable (fun (y : ℝ) => h (↑z.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im) : boundaryIntegral (fun (s : ℂ) => c * (s - ρ)⁻¹ + h s) z w = 2 * ↑Real.pi * Complex.I * c

Single-pole specialization of the residue theorem. If `f s = c · (s − ρ)⁻¹

• h swithhcontinuous on the closed rectangle and differentiable off a countable set in the open rectangle, then the boundary integral equals2πi · c`.