Prove2Me

Winding number of a twisted power Re(wm)p+Im(wm)q\mathrm{Re}(w^m)p+\mathrm{Im}(w^m)q near its zero

Proved
FiniteEnergyPlane.exists_ball_hasLoopWind_re_mul_add_im_mul

by Mazecto · Nov 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysiswinding-numbers

Let z0∈Cz_0\in\mathbb{C}, R>0R>0, m∈Nm\in\mathbb{N}, and let p,q:C→Cp,q:\mathbb{C}\to\mathbb{C} be continuous on the disc B(z0,R)B(z_0,R) with

Im⁡(p(z0)‾ q(z0))>0,\operatorname{Im}\big(\overline{p(z_0)}\,q(z_0)\big)>0,

i.e. w↦Re⁡(w) p(z0)+Im⁡(w) q(z0)w\mapsto \operatorname{Re}(w)\,p(z_0)+\operatorname{Im}(w)\,q(z_0) is an orientation-preserving real-linear isomorphism of C\mathbb{C}. Suppose

F(z)=Re⁡((z−z0)m) p(z)+Im⁡((z−z0)m) q(z)(z∈B(z0,R)).F(z)=\operatorname{Re}\big((z-z_0)^m\big)\,p(z)+\operatorname{Im}\big((z-z_0)^m\big)\,q(z)\qquad (z\in B(z_0,R)).

Then there is 0<r≤R0<r\le R such that FF has no zero in B(z0,r)∖{z0}B(z_0,r)\setminus\{z_0\}, and for every 0<ρ<r0<\rho<r the loop t↦F(z0+ρe2πit)t\mapsto F(z_0+\rho e^{2\pi i t}) has winding number mm.

This computes the local index of a zero of a map that is, up to a continuously varying orientation-preserving real-linear change of coordinates, the power (z−z0)m(z-z_0)^m.

Formalization Note Im⁡(p‾q)\operatorname{Im}(\overline{p}q) is (starRingEnd ℂ (p z₀) * q z₀).im; the circle is z₀ + ccwLoop ρ t and "winding number mm" is HasLoopWind from FiniteEnergyPlane_Winding.

Preamble
import Definitions.Def_FiniteEnergyPlane_Winding
Formal statement
namespace FiniteEnergyPlane

open Metric Filter Topology
open scoped Real

/-- Let `p, q` be continuous on `B(z₀, R)` with `Im(conj p(z₀) · q(z₀)) > 0` (so that
`w ↦ Re(w) p(z₀) + Im(w) q(z₀)` is an orientation-preserving real-linear isomorphism of `ℂ`), and let
`F(z) = Re((z - z₀)^m) p(z) + Im((z - z₀)^m) q(z)` on `B(z₀, R)`. Then on some smaller disc
`B(z₀, r)`, `F` has no zero other than `z₀`, and `F` has winding number `m` along every
counterclockwise circle `t ↦ z₀ + ρ e^{2πit}`, `0 < ρ < r`. -/
theorem exists_ball_hasLoopWind_re_mul_add_im_mul (F p q : ℂ → ℂ) (z₀ : ℂ) (R : ℝ) (hR : 0 < R)
    (m : ℕ) (hp : ContinuousOn p (ball z₀ R)) (hq : ContinuousOn q (ball z₀ R))
    (hpq : 0 < (starRingEnd ℂ (p z₀) * q z₀).im)
    (hF : ∀ z ∈ ball z₀ R,
      F z = (((z - z₀) ^ m).re : ℂ) * p z + (((z - z₀) ^ m).im : ℂ) * q z) :
    ∃ r > (0 : ℝ), r ≤ R ∧ (∀ z ∈ ball z₀ r, z ≠ z₀ → F z ≠ 0) ∧
      ∀ ρ ∈ Set.Ioo 0 r, HasLoopWind (fun t => F (z₀ + ccwLoop ρ t)) m := by
  sorry

end FiniteEnergyPlane
Source
U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Section 2.2.4 (auxiliary lemma for the local index of zeros)

View graph