Strip coordinates for a punctured disk: a centre from which finitely many interior points lie on distinct rays
ProvedHryniewiczCriterion.exists_strip_centerdynamical-systemsgeometry-topologysymplectic-geometry
Let be a finite set of points of the open unit disk and write (circlePoint). Then there is a centre such that, in the "strip coordinates" , every has unique coordinates: there are and with , and with forces and . Moreover distinct points of have , i.e. they lie on distinct rays from .
Proof. Choose off the finitely many lines through two points of and off (a finite union of lines is Lebesgue-null and has positive measure). For the ray from through leaves the disk at a unique point , at distance from (the positive root of ); put . If then (as ) and is a positive multiple of , so and . If then are collinear, which was excluded.
Preamble
import Definitions.Def_HryniewiczCriterion_GlobalSection import Definitions.Def_HryniewiczCriterion_SelfLinking open HryniewiczCriterion
Formal statement
theorem HryniewiczCriterion.exists_strip_center (Z : Finset Plane) (hZ : ∀ z ∈ Z, z ∈ openUnitDisk) :
∃ c : Plane, c ∈ openUnitDisk ∧ ∃ lam sp : Plane → ℝ, ∀ z ∈ Z,
0 < lam z ∧ lam z < 1 ∧ z = c + lam z • (circlePoint (sp z) - c) ∧
(∀ μ s : ℝ, 0 ≤ μ → c + μ • (circlePoint s - c) = z → μ = lam z ∧ ∃ n : ℤ, s = sp z + n) ∧
(∀ w ∈ Z, w ≠ z → ∀ n : ℤ, sp w ≠ sp z + n) := by sorrySource
Elementary plane geometry (used for the residue formula for the Gauss linking integral)