Winding interval width of pair bound

Proved

BirkhoffGlobalSection.winding_interval_width_of_pair_bound

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

dynamical-systemstopology

If an attained winding image is [a,b] and every two values differ by less than one half, its width b−a is strictly less than one half.

All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.

Preamble

import Theorems.Thm_BirkhoffGlobalSection_contact_winding_width_bundle
open BirkhoffGlobalSection Set Filter Topology
open scoped ContDiff Topology
set_option linter.unusedVariables false


set_option autoImplicit false
set_option maxHeartbeats 800000

Formal statement

theorem BirkhoffGlobalSection.winding_interval_width_of_pair_bound :
∀ (d : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b)
    (himage : d '' Icc 0 (2 * Real.pi) = Icc a b)
    (hbound : ∀ s r, |d r - d s| < 1 / 2),
    b - a < 1 / 2 := by sorry

Source

Independent extraction of component 5 of the Proved theorem BirkhoffGlobalSection.contact_winding_width_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_winding_width_bundle.lean. Exact original component retained.

View graph