Sector Curve PV Computation (Lemma 3.1)

Model sector-curve and PV integral computations for Laurent series terms. This implements the key computation from Hungerbuhler-Wasem (arXiv:1808.00997v2) Lemma 3.1: the principal value of dz/z along a sector curve equals i * alpha, where alpha is the opening angle of the sector.

Main Definitions

• sectorCurve -- the model sector-curve parameterized on [0,3]

Main Results

• pv_sector_dz_over_z -- PV of dz/z along sector curve equals I * alpha

See SectorCurveLemma.lean for higher-order results (pv_sector_higher_power, cauchyPV_sectorCurve_simplePole, etc.).

Mathematical Overview

The sector curve sigma_{r,alpha} is a closed curve from the origin, along the positive real axis to radius r, then around an arc of angle alpha, then back to the origin along the ray at angle alpha. Specifically:

• Segment 1 (t in [0,1]): radial ray t |-> t * r (outgoing along real axis)
• Segment 2 (t in [1,2]): arc t |-> r * exp(i * (t-1) * alpha) at radius r
• Segment 3 (t in [2,3]): radial ray t |-> (3-t) * r * exp(i * alpha) (returning)

The PV of dz/z along this curve decomposes as:

• Segments 1 and 3 contribute symmetric logarithmic divergences that cancel
• Segment 2 contributes int_0^alpha i d theta = i * alpha

Reference: Hungerbuhler-Wasem, arXiv:1808.00997v2, Lemma 3.1.

Definition of the sector curve

noncomputable def sectorCurve (r α t : ℝ) : ℂ

The model sector curve parameterized on [0,3].

• [0,1]: radial ray from 0 to r along the positive real axis
• [1,2]: circular arc of radius r from angle 0 to angle alpha
• [2,3]: radial ray from rexp(ialpha) back to 0

Equations

• sectorCurve r α t = if t ≤ 1 then ↑(t * r) else if t ≤ 2 then ↑r * Complex.exp (Complex.I * ↑((t - 1) * α)) else ↑((3 - t) * r) * Complex.exp (Complex.I * ↑α)

Basic properties of the sector curve

theorem sectorCurve_zero (r α : ℝ) : sectorCurve r α 0 = 0

The sector curve at t=0 is 0.

theorem sectorCurve_three (r α : ℝ) : sectorCurve r α 3 = 0

The sector curve at t=3 is 0.

theorem sectorCurve_closed (r α : ℝ) : sectorCurve r α 0 = sectorCurve r α 3

The sector curve is a closed curve (starts and ends at 0).

theorem sectorCurve_one (r α : ℝ) : sectorCurve r α 1 = ↑r

The sector curve at t=1 is r (the transition from radial to arc).

theorem sectorCurve_two (r α : ℝ) : sectorCurve r α 2 = ↑r * Complex.exp (Complex.I * ↑α)

The sector curve at t=2 is r * exp(i * alpha) (end of arc).

theorem sectorCurve_seg1 (r α t : ℝ) (ht : t ∈ Set.Icc 0 1) : sectorCurve r α t = ↑(t * r)

Segment 1: for t in [0,1], the sector curve is t * r.

theorem sectorCurve_seg2 (r α t : ℝ) (ht : t ∈ Set.Icc 1 2) : sectorCurve r α t = ↑r * Complex.exp (Complex.I * ↑((t - 1) * α))

Segment 2: for t in [1,2], the sector curve is r * exp(i*(t-1)*alpha).

theorem sectorCurve_seg3 (r α t : ℝ) (ht : t ∈ Set.Icc 2 3) : sectorCurve r α t = ↑((3 - t) * r) * Complex.exp (Complex.I * ↑α)

Segment 3: for t in [2,3], the sector curve is (3-t)*r * exp(i*alpha).

theorem sectorCurve_continuousOn (r α : ℝ) : ContinuousOn (sectorCurve r α) (Set.Icc 0 3)

The sector curve is continuous on [0,3].

theorem sectorCurve_passes_through_origin (r α : ℝ) : sectorCurve r α 0 = 0 ∧ sectorCurve r α 3 = 0

The sector curve passes through the origin at t=0 and t=3.

theorem sectorCurve_norm_on_arc (r : ℝ) (hr : 0 < r) (α t : ℝ) (ht : t ∈ Set.Icc 1 2) : ‖sectorCurve r α t‖ = r

On the arc segment (t in [1,2]), the sector curve has modulus r.

Derivative of the sector curve

theorem deriv_sectorCurve_seg1 (r α t : ℝ) (ht : t ∈ Set.Ioo 0 1) : deriv (sectorCurve r α) t = ↑r

Derivative on segment 1 (t in (0,1)): deriv (sectorCurve r alpha) t = r.

theorem deriv_sectorCurve_seg2 (r α t : ℝ) (ht : t ∈ Set.Ioo 1 2) : deriv (sectorCurve r α) t = ↑r * (Complex.I * ↑α) * Complex.exp (Complex.I * ↑((t - 1) * α))

Derivative on segment 2 (t in (1,2)): deriv (sectorCurve r alpha) t = r * (I * alpha) * exp(I * (t-1) * alpha).

theorem deriv_sectorCurve_seg3 (r α t : ℝ) (ht : t ∈ Set.Ioo 2 3) : deriv (sectorCurve r α) t = -↑r * Complex.exp (Complex.I * ↑α)

Derivative on segment 3 (t in (2,3)): deriv (sectorCurve r alpha) t = -r * exp(I * alpha).

PV integrand analysis

theorem pv_integrand_seg1 (r : ℝ) (hr : 0 < r) (α t : ℝ) (ht : t ∈ Set.Ioo 0 1) : (sectorCurve r α t)⁻¹ * deriv (sectorCurve r α) t = ↑t⁻¹

The integrand (sectorCurve r alpha t)^(-1) * deriv (sectorCurve r alpha) t on segment 1 (t in (0,1)) simplifies to 1/t (as a complex number).

theorem pv_integrand_seg2 (r : ℝ) (hr : 0 < r) (α t : ℝ) (ht : t ∈ Set.Ioo 1 2) : (sectorCurve r α t)⁻¹ * deriv (sectorCurve r α) t = Complex.I * ↑α

The integrand on segment 2 (t in (1,2)) simplifies to I * alpha.

theorem pv_integrand_seg3 (r : ℝ) (hr : 0 < r) (α t : ℝ) (ht : t ∈ Set.Ioo 2 3) : (sectorCurve r α t)⁻¹ * deriv (sectorCurve r α) t = -↑(3 - t)⁻¹

The integrand on segment 3 (t in (2,3)) simplifies to -1/(3-t).

PV computation: Lemma 3.1

theorem integral_seg1_eq_neg_log (ε : ℝ) (hε : 0 < ε) (_hε1 : ε < 1) : ∫ (t : ℝ) in ε..1, t⁻¹ = -Real.log ε

The integral of 1/t from epsilon to 1 is -log(epsilon).

theorem integral_seg3_eq_log (ε : ℝ) (hε : 0 < ε) (_hε1 : ε < 1) : ∫ (t : ℝ) in 2..3 - ε, -(3 - t)⁻¹ = Real.log ε

The integral of -1/(3-t) from 2 to 3-epsilon is log(epsilon).

theorem sectorCurve_norm_seg1 (r : ℝ) (hr : 0 < r) (α t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖sectorCurve r α t‖ = t * r

On segment 1, the norm of the sector curve is t * r.

theorem sectorCurve_norm_seg3' (r : ℝ) (hr : 0 < r) (α t : ℝ) (ht : t ∈ Set.Icc 2 3) : ‖sectorCurve r α t‖ = (3 - t) * r

On segment 3, the norm of the sector curve is (3 - t) * r.

theorem log_cancellation (r : ℝ) (hr : 0 < r) (ε : ℝ) (hε : 0 < ε) (hεr : ε < r) : (∫ (t : ℝ) in ε / r..1, ↑t⁻¹) + ∫ (t : ℝ) in 2..3 - ε / r, -↑(3 - t)⁻¹ = 0

The logarithmic integrals from segments 1 and 3 cancel.

theorem pv_sector_cutoff_eq (r : ℝ) (hr : 0 < r) (α ε : ℝ) (hε : 0 < ε) (hεr : ε < r) : (∫ (t : ℝ) in 0..3, if ‖sectorCurve r α t - 0‖ > ε then (sectorCurve r α t)⁻¹ * deriv (sectorCurve r α) t else 0) = Complex.I * ↑α

For 0 < ε < r, the PV cutoff integral of dz/z along the sector curve equals I * α. This is the key cancellation lemma: the logarithmic divergences from segments 1 and 3 cancel.

theorem pv_sector_dz_over_z (r : ℝ) (hr : 0 < r) (α : ℝ) (_hα_nonneg : 0 ≤ α) (_hα_le : α ≤ 2 * Real.pi) : CauchyPrincipalValueExists' (fun (z : ℂ) => z⁻¹) (sectorCurve r α) 0 3 0 ∧ cauchyPrincipalValue' (fun (z : ℂ) => z⁻¹) (sectorCurve r α) 0 3 0 = Complex.I * ↑α

Lemma 3.1 (dz/z part): The principal value of dz/z along the sector curve from 0 to 3 equals I * alpha.

The divergences from the radial segments cancel, leaving only the arc contribution.