Bridge to Mathlib Circle Integrals

Connects the project's generalizedWindingNumber' (defined via Cauchy principal value) to mathlib's circleIntegral for the case of circular contours.

Mathlib does not define a general winding number, but it provides:

• circleIntegral f c R -- the integral ∮ z in C(c,R), f z
• circleIntegral.integral_sub_inv_of_mem_ball -- ∮ z in C(c,R), (z-w)⁻¹ = 2πi when w ∈ ball c R

This file shows that for circleMap c R over [0, 2π], the project's generalizedWindingNumber' agrees with the classical contour integral formula, which in turn equals (2πi)⁻¹ * circleIntegral (· - w)⁻¹ c R.

Main Results

• contourIntegral_circleMap_eq_circleIntegral -- the interval integral ∫ θ in 0..2π, f(circleMap c R θ) * deriv(circleMap c R) θ equals mathlib's ∮ z in C(c,R), f z
• generalizedWindingNumber_circleMap_eq_inv_circleIntegral -- when circleMap c R avoids w, the generalized winding number equals (2πi)⁻¹ * ∮ z in C(c,R), (z - w)⁻¹
• generalizedWindingNumber_circleMap_eq_one_of_mem_ball -- for w ∈ ball c R with R > 0, the generalized winding number of circleMap c R around w equals 1, via mathlib's integral_sub_inv_of_mem_ball

theorem contourIntegral_circleMap_eq_circleIntegral (f : ℂ → ℂ) (c : ℂ) (R : ℝ) : ∫ (θ : ℝ) in 0..2 * Real.pi, f (circleMap c R θ) * deriv (circleMap c R) θ = ∮ (z : ℂ) in C(c, R), f z

The interval integral ∫ θ in 0..2π, f(circleMap c R θ) * deriv(circleMap c R) θ equals mathlib's circle integral ∮ z in C(c,R), f z.

This is the key bridge: mathlib defines circleIntegral using smul (scalar multiplication deriv(circleMap c R) θ • f(circleMap c R θ)), while the project uses mul (pointwise multiplication f(γ t) * deriv γ t). For ℂ-valued functions, smul and mul coincide.

theorem generalizedWindingNumber_circleMap_eq_inv_circleIntegral (c w : ℂ) (R : ℝ) (hR : 0 < R) (hw : ‖w - c‖ ≠ R) : generalizedWindingNumber' (circleMap c R) 0 (2 * Real.pi) w = (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(c, R), (z - w)⁻¹

The generalized winding number of circleMap c R around w (for a point not on the circle) equals (2πi)⁻¹ * ∮ z in C(c,R), (z - w)⁻¹.

This combines generalizedWindingNumber_eq_classical_away (which shows the PV winding number equals the classical integral when the curve avoids w) with contourIntegral_circleMap_eq_circleIntegral (which identifies the classical integral with mathlib's circleIntegral).

theorem generalizedWindingNumber_circleMap_eq_one_of_mem_ball (c w : ℂ) (R : ℝ) (hR : 0 < R) (hw : w ∈ Metric.ball c R) : generalizedWindingNumber' (circleMap c R) 0 (2 * Real.pi) w = 1

The generalized winding number of circleMap c R around a point w inside the circle equals 1.

This is the definitive bridge between the project's generalizedWindingNumber' and mathlib's circle integral theory. The proof factors through mathlib's circleIntegral.integral_sub_inv_of_mem_ball, which computes ∮ z in C(c,R), (z-w)⁻¹ = 2πi.

theorem circleMap_contourIntegral_sub_inv_eq_two_pi_I (c w : ℂ) (R : ℝ) (_hR : 0 < R) (hw : w ∈ Metric.ball c R) : ∫ (θ : ℝ) in 0..2 * Real.pi, (circleMap c R θ - w)⁻¹ * deriv (circleMap c R) θ = 2 * ↑Real.pi * Complex.I

The classical contour integral of (z - w)⁻¹ around a circle containing w equals 2πi, expressed in the project's interval integral format.

This is a convenience wrapper: it states the result purely in terms of interval integrals (no circleIntegral notation), useful for downstream proofs that work with ∫ t in a..b, ... rather than ∮.