Prove2Me

Homotopy invariance of the winding integral ∫01F′/F\int_0^1 F'/F

Proved
logDeriv_intervalIntegral_eq_of_homotopy

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

analysiscomplex-analysistopology

Let F:[0,1]×R→C∖{0}F:[0,1]\times\mathbb{R}\to\mathbb{C}\setminus\{0\} be continuous, differentiable in ss with ∂sF\partial_sF continuous on [0,1]×R[0,1]\times\mathbb{R}, and closed in ss: F(r,1)=F(r,0)F(r,1)=F(r,0). Then the winding integral does not depend on rr:

∫01∂sF(1,s)F(1,s) ds=∫01∂sF(0,s)F(0,s) ds.\int_0^1\frac{\partial_sF(1,s)}{F(1,s)}\,ds=\int_0^1\frac{\partial_sF(0,s)}{F(0,s)}\,ds.

Each integral lies in 2πiZ2\pi i\mathbb{Z} because F(r,s)=F(r,0)exp⁡∫0s∂sF/FF(r,s)=F(r,0)\exp\int_0^s\partial_sF/F. It is continuous in rr, hence constant.

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 logDeriv_intervalIntegral_eq_of_homotopy {F F' : ℝ → ℝ → ℂ}
    (hF : ∀ r ∈ Set.Icc (0 : ℝ) 1, ∀ s, HasDerivAt (F r) (F' r s) s)
    (hcF : ContinuousOn (Function.uncurry F) (Set.Icc 0 1 ×ˢ Set.univ))
    (hcF' : ContinuousOn (Function.uncurry F') (Set.Icc 0 1 ×ˢ Set.univ))
    (hne : ∀ r ∈ Set.Icc (0 : ℝ) 1, ∀ s, F r s ≠ 0)
    (hper : ∀ r ∈ Set.Icc (0 : ℝ) 1, F r 1 = F r 0) :
    ∫ s in (0 : ℝ)..1, F' 1 s / F 1 s = ∫ s in (0 : ℝ)..1, F' 0 s / F 0 s := 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