A periodic immersion onto the circle is a -fold cover with , and the Gauss integral of its image loop is times that of the standard circle
ProvedHryniewiczCriterion.gaussLinkingIntegral_circle_immersiondynamical-systemsgeometry-topologysymplectic-geometry
Let be a map of period with everywhere. Then is onto , and for a lift with , (if , would be periodic, hence have a critical point, where ).
Let be near with on , let be a loop of period missing , and let miss both. Then
with gaussLinkingIntegral as .
Suggested proof. The straight-line homotopy keeps the loops inside , so homotopy invariance (gaussIntegral_eq_of_homotopy) gives . For use the symmetry of the Gauss integrand and gaussLinkingIntegral_comp_mul_nat; for additionally reverse the loop, which changes the sign.
Preamble
import Definitions.Def_HryniewiczCriterion_GlobalSection import Definitions.Def_HryniewiczCriterion_SelfLinking open HryniewiczCriterion
Formal statement
theorem HryniewiczCriterion.gaussLinkingIntegral_circle_immersion (E : Plane → R4) (U : Set Plane) (hU : IsOpen U) (hCU : unitCircle ⊆ U)
(hE : ContDiffOn ℝ 2 E U) (hEunit : ∀ v ∈ unitCircle, euclidNorm (E v) = 1)
(u : ℝ → Plane) (hu : ContDiff ℝ 2 u) (huper : ∀ s, u (s + 1) = u s)
(hucirc : ∀ s, u s ∈ unitCircle) (hu' : ∀ s, deriv u s ≠ 0)
(γ : ℝ → R4) (hγ : ContDiff ℝ 2 γ) (hγper : ∀ t, γ (t + 1) = γ t)
(hγunit : ∀ t, euclidNorm (γ t) = 1) (hbd : ∀ s t, E (u s) ≠ γ t)
(N : R4) (hN : euclidNorm N = 1) (hNγ : ∀ t, γ t ≠ N) (hNE : ∀ s, E (u s) ≠ N) :
(∀ w ∈ unitCircle, ∃ s, u s = w) ∧ ∃ k : ℤ, k ≠ 0 ∧
gaussLinkingIntegral N (fun s => E (u s)) γ =
k * gaussLinkingIntegral N (fun s => E (circlePoint s)) γ := by sorrySource
Elementary (lifting of circle maps and the multiplicativity of the Gauss integral); used for the boundary parametrization in U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014) 791-862, arXiv:1105.2077, Lemma 3.12.