A function close to one with nonzero boundary winding has a zero in the disc

Proved

FiniteEnergyPlane.exists_eq_zero_of_hasLoopWind_of_norm_sub_lt

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

topology-of-the-planewinding-number

Let $c\in\mathbb{C}$ , $R>0$ , and $g,h:\mathbb{C}\to\mathbb{C}$ . Suppose $g$ is continuous on $\bar B(c,R)$ , the loop $t\mapsto h(c+Re^{2\pi i t})$ lies in $\mathbb{C}\setminus\{0\}$ with winding number $k\neq 0$ , and $|g-h|<|h|$ on the circle $|z-c|=R$ . Then $g$ has a zero in $\bar B(c,R)$ .

Role: a topological existence principle for zeros of continuous functions, with no differentiability of $g$ assumed.

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

open Metric

/-- Let `h` have nonzero winding number along the circle of radius `R` about `c`, and let `g` be
continuous on the closed disc with `‖g - h‖ < ‖h‖` on that circle. Then `g` has a zero in the
closed disc. -/
theorem exists_eq_zero_of_hasLoopWind_of_norm_sub_lt (g h : ℂ → ℂ) (c : ℂ) (R : ℝ) (hR : 0 < R)
    (hg : ContinuousOn g (closedBall c R)) (k : ℤ) (hk : k ≠ 0)
    (hw : HasLoopWind (fun t => h (c + ccwLoop R t)) k)
    (hclose : ∀ t : ℝ, ‖g (c + ccwLoop R t) - h (c + ccwLoop R t)‖ < ‖h (c + ccwLoop R t)‖) :
    ∃ z ∈ closedBall c R, g z = 0 := by
  sorry

end FiniteEnergyPlane

Source

Standard Rouché-type statement for continuous functions in the plane

View graph