Smooth polar form of a loop with winding number one

Proved

exists_smooth_polar_of_logDeriv_integral_eq_two_pi_I

by Mazecto · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscomplex-analysis

Let $c:\mathbb{R}\to\mathbb{C}\setminus\{0\}$ be smooth and $1$ -periodic with $\int_0^1 c'/c=2\pi i$ . Then there are smooth $r,\theta:\mathbb{R}\to\mathbb{R}$ with $r>0$ and $1$ -periodic, $\theta(s+1)=\theta(s)+2\pi$ , and $c=r\,e^{i\theta}$ . Take $L(s)=\int_0^s c'/c$ . Then $c=c(0)e^{L}$ , so $r=|c(0)|e^{\operatorname{Re}L}$ and $\theta=\arg c(0)+\operatorname{Im}L$ work.

Preamble

import Mathlib.Analysis.SpecialFunctions.Complex.Arg
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.Analysis.Calculus.ContDiff.Defs

open scoped ContDiff

Formal statement

theorem exists_smooth_polar_of_logDeriv_integral_eq_two_pi_I {c : ℝ → ℂ} (hc : ContDiff ℝ ∞ c) (hne : ∀ s, c s ≠ 0)
    (hper : ∀ s, c (s + 1) = c s)
    (hW : ∫ s in (0 : ℝ)..1, deriv c s / c s = 2 * Real.pi * Complex.I) :
    ∃ r θ : ℝ → ℝ, ContDiff ℝ ∞ r ∧ ContDiff ℝ ∞ θ ∧ (∀ s, 0 < r s) ∧
      (∀ s, r (s + 1) = r s) ∧ (∀ s, θ (s + 1) = θ s + 2 * Real.pi) ∧
      ∀ s, c s = (r s : ℂ) * (Real.cos (θ s) + Real.sin (θ s) * Complex.I) := by sorry

Source

Standard winding-number calculus for C^1 loops in C \ {0}; used for the conormal winding of a disk-like global surface of section in Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Theorem 1.7 (via Hryniewicz, Trans. AMS 364 (2012), Prop. 2.1).

View graph