Sector Curve PV Lemmas

Higher-order PV computations and the generalized winding number for the model sector-curve defined in SectorCurve.lean.

Main Results

• pv_sector_higher_power -- for n >= 1, PV int z^{n-1} dz = 0 (angle condition)
• cauchyPV_sectorCurve_simplePole -- Lemma 3.1 for simple poles: PV = I * alpha * residue
• cauchyPV_sectorCurve_eq_mul_residueSimplePole -- variant for arbitrary f = c/z + g
• pv_sector_negative_power -- Equation (3.4): PV of z^{-n} is 0 under angle condition
• generalizedWindingNumber_sectorCurve -- winding number equals alpha / (2 * pi)

theorem pv_sector_higher_power (r : ℝ) (_hr : 0 < r) (α : ℝ) (_hα_nonneg : 0 ≤ α) (_hα_le : α ≤ 2 * Real.pi) (n : ℕ) (hn : 1 ≤ n) (_h_angle : ∃ (k : ℤ), ↑n * α = ↑k * (2 * Real.pi)) : ∫ (t : ℝ) in 0..3, sectorCurve r α t ^ (n - 1) * deriv (sectorCurve r α) t = 0

For n >= 1, the integral of z^(n-1) dz along the sector curve is 0 when n * alpha is a multiple of 2 * pi.

theorem cauchyPV_sectorCurve_simplePole (r : ℝ) (hr : 0 < r) (α : ℝ) (hα_nonneg : 0 ≤ α) (hα_le : α ≤ 2 * Real.pi) (c : ℂ) (g : ℂ → ℂ) (hg : AnalyticOnNhd ℂ g (Metric.ball 0 (r + 1))) : CauchyPrincipalValueExists' (fun (z : ℂ) => c / z + g z) (sectorCurve r α) 0 3 0 ∧ cauchyPrincipalValue' (fun (z : ℂ) => c / z + g z) (sectorCurve r α) 0 3 0 = Complex.I * ↑α * c

Lemma 3.1 (Simple pole version): For f(z) = c/z + g(z) where g is analytic on a ball containing the sector, the principal value along the sector curve equals I * α * c.

The hypotheses require g analytic on a ball strictly containing the sector image (to guarantee a primitive exists) and f = c/z + g at all nonzero points.

theorem cauchyPV_sectorCurve_eq_mul_residueSimplePole (r : ℝ) (hr : 0 < r) (α : ℝ) (hα_nonneg : 0 ≤ α) (hα_le : α ≤ 2 * Real.pi) (f : ℂ → ℂ) (c : ℂ) (g : ℂ → ℂ) (hg : AnalyticOnNhd ℂ g (Metric.ball 0 (r + 1))) (hf_eq : ∀ (z : ℂ), z ≠ 0 → f z = c / z + g z) (hc : c = residueSimplePole f 0) : CauchyPrincipalValueExists' f (sectorCurve r α) 0 3 0 ∧ cauchyPrincipalValue' f (sectorCurve r α) 0 3 0 = Complex.I * ↑α * residueSimplePole f 0

Variant of Lemma 3.1: for an arbitrary f equal to c/z + g at nonzero points, with g analytic on a ball containing the sector, the PV equals I * α * c.

theorem pv_sector_negative_power (r : ℝ) (hr : 0 < r) (α : ℝ) (_hα_nonneg : 0 ≤ α) (_hα_le : α ≤ 2 * Real.pi) (n : ℕ) (hn : 2 ≤ n) (h_angle : ∃ (k : ℤ), ↑↑(n - 1) * α = ↑k * (2 * Real.pi)) : CauchyPrincipalValueExists' (fun (z : ℂ) => z ^ (-↑n)) (sectorCurve r α) 0 3 0 ∧ cauchyPrincipalValue' (fun (z : ℂ) => z ^ (-↑n)) (sectorCurve r α) 0 3 0 = 0

Equation (3.4): The PV of z^{-n} along the sector curve is 0 when (n-1) * α is a multiple of 2π. The cutoff integral equals ε^{1-n} * (exp(i(1-n)α) - 1) / (1-n), which vanishes identically under the angle condition. By FTC with primitive F(t) = γ(t)^{1-n}/(1-n).

theorem generalizedWindingNumber_sectorCurve (r : ℝ) (hr : 0 < r) (α : ℝ) (hα_nonneg : 0 ≤ α) (hα_le : α ≤ 2 * Real.pi) (_hPV : CauchyPrincipalValueExists' (fun (z : ℂ) => z⁻¹) (sectorCurve r α) 0 3 0) : generalizedWindingNumber' (sectorCurve r α) 0 3 0 = ↑α / (2 * ↑Real.pi)

The generalized winding number of the sector curve around 0 equals alpha / (2 * pi).