Hopf's Umlaufsatz

AbbreviationEuclidean plane for the Umlaufsatz#✓fully proved

The Euclidean plane is the space \(\mathbb{R}^2\) of pairs of real numbers with the Euclidean inner product and norm.

abbrev Plane := EuclideanSpace ℝ (Fin 2)

Used by 6

Used byPlanar determinant for the Umlaufsatz · Hopf's Umlaufsatz · Positively oriented simple closed unit-speed curve · Tangent-angle lift · Signed area of a closed plane curve · Velocity of a plane curve

DefinitionParameter period for the Umlaufsatz#✓fully proved

The parameter period of the closed curves in the Hopf Umlaufsatz is the real number \(2\pi\).

noncomputable def period : ℝ := 2 * Real.pi

Used by 3

Used byPositively oriented simple closed unit-speed curve · Signed area of a closed plane curve · Total signed curvature of a tangent-angle lift

DefinitionVelocity of a plane curve#✓fully proved

For a curve \(r : \mathbb{R} \to \mathbb{R}^2\) in the Euclidean plane and \(t \in \mathbb{R}\), the velocity of \(r\) at \(t\) is its derivative \(r'(t) \in \mathbb{R}^2\), taken to be \(0\) where \(r\) is not differentiable.

noncomputable def velocity (r : ℝ → Plane) (t : ℝ) : Plane := deriv r t

Uses 1 · Used by 3

Statement usesEuclidean plane for the Umlaufsatz

Used byPositively oriented simple closed unit-speed curve · Tangent-angle lift · Signed area of a closed plane curve

DefinitionPlanar determinant for the Umlaufsatz#✓fully proved

For vectors \(u = (u_0, u_1)\) and \(v = (v_0, v_1)\) in the Euclidean plane \(\mathbb{R}^2\), \(\det(u, v) = u_0 v_1 - u_1 v_0\), the signed area of the parallelogram spanned by \(u\) and \(v\).

def det2 (u v : Plane) : ℝ := u 0 * v 1 - u 1 * v 0

Uses 1 · Used by 1

Statement usesEuclidean plane for the Umlaufsatz

Used bySigned area of a closed plane curve

DefinitionSigned area of a closed plane curve#✓fully proved

For a curve \(r : \mathbb{R} \to \mathbb{R}^2\), the signed area is \(\frac{1}{2}\int_0^{2\pi} \det(r(t), r'(t))\,dt\), where \(r'\) is the velocity of \(r\) and \(\det(u, v) = u_0 v_1 - u_1 v_0\) (Green's normalization). Its sign fixes the orientation convention.

noncomputable def signedArea (r : ℝ → Plane) : ℝ :=
  (1 / 2 : ℝ) * ∫ t in (0 : ℝ)..period, det2 (r t) (velocity r t)

Uses 4 · Used by 1

Statement usesEuclidean plane for the Umlaufsatz · Planar determinant for the Umlaufsatz · Parameter period for the Umlaufsatz · Velocity of a plane curve

Used byPositively oriented simple closed unit-speed curve

StructurePositively oriented simple closed unit-speed curve#✓fully proved

A curve \(r : \mathbb{R} \to \mathbb{R}^2\) in the Euclidean plane is a positively oriented simple closed unit-speed curve when it is continuously differentiable, periodic with period \(2\pi\), injective on \([0, 2\pi)\), has velocity of norm \(\lVert r'(t) \rVert = 1\) for every \(t \in \mathbb{R}\), and has positive signed area \(\frac{1}{2}\int_0^{2\pi} \det(r(t), r'(t))\,dt > 0\), where \(\det(u, v) = u_0 v_1 - u_1 v_0\).

structure IsPositiveSimpleClosedUnitSpeedCurve (r : ℝ → Plane) : Prop where
  smooth : ContDiff ℝ 1 r
  periodic : Function.Periodic r period
  injective_on_period : Set.InjOn r (Set.Ico (0 : ℝ) period)
  unit_speed : ∀ t : ℝ, ‖velocity r t‖ = 1
  positive_orientation : 0 < signedArea r

Uses 4 · Used by 1

Statement usesEuclidean plane for the Umlaufsatz · Parameter period for the Umlaufsatz · Signed area of a closed plane curve · Velocity of a plane curve

Used byHopf's Umlaufsatz

StructureTangent-angle lift#✓fully proved

For a curve \(r : \mathbb{R} \to \mathbb{R}^2\) in the Euclidean plane, a function \(\alpha : \mathbb{R} \to \mathbb{R}\) is a tangent-angle lift of \(r\) when \(\alpha\) is continuously differentiable and the velocity of \(r\) satisfies \(r'(t) = (\cos \alpha(t), \sin \alpha(t))\) for every \(t \in \mathbb{R}\).

structure IsTangentAngleLift (r : ℝ → Plane) (α : ℝ → ℝ) : Prop where
  smooth : ContDiff ℝ 1 α
  velocity_eq : ∀ t : ℝ,
    velocity r t = !₂[Real.cos (α t), Real.sin (α t)]

Uses 2 · Used by 1

Statement usesEuclidean plane for the Umlaufsatz · Velocity of a plane curve

Used byHopf's Umlaufsatz

DefinitionSigned curvature#✓fully proved

For a function \(\alpha : \mathbb{R} \to \mathbb{R}\) and \(t \in \mathbb{R}\), the signed curvature of \(\alpha\) at \(t\) is the derivative \(\alpha'(t)\), taken to be \(0\) where \(\alpha\) is not differentiable at \(t\).

When \(\alpha\) is a tangent-angle lift of a unit-speed plane curve, this is the signed curvature of the curve at \(t\).

noncomputable def signedCurvature (α : ℝ → ℝ) (t : ℝ) : ℝ := deriv α t

Used by 1

Used byTotal signed curvature of a tangent-angle lift

DefinitionTotal signed curvature of a tangent-angle lift#✓fully proved

For a function \(\alpha : \mathbb{R} \to \mathbb{R}\), the total signed curvature is \(\int_0^{2\pi} \alpha'(t)\,dt\), the integral of the signed curvature \(\alpha'\) over one parameter period \([0, 2\pi]\).

noncomputable def totalCurvature (α : ℝ → ℝ) : ℝ :=
  ∫ t in (0 : ℝ)..period, signedCurvature α t

Uses 2 · Used by 1

Statement usesParameter period for the Umlaufsatz · Signed curvature

Used byHopf's Umlaufsatz

TheoremHopf's Umlaufsatz#●ready to prove

Let \(r : \mathbb{R} \to \mathbb{R}^2\) be a positively oriented simple closed unit-speed plane curve: \(r\) is continuously differentiable and \(2\pi\)-periodic, injective on \([0, 2\pi)\), satisfies \(\lVert r'(t) \rVert = 1\) for all \(t\), and has positive signed area \(\frac{1}{2}\int_0^{2\pi} \det(r(t), r'(t))\,dt > 0\), where \(\det(u, v) = u_0 v_1 - u_1 v_0\). Let \(\alpha : \mathbb{R} \to \mathbb{R}\) be a continuously differentiable tangent-angle lift of \(r\), that is, \(r'(t) = (\cos \alpha(t), \sin \alpha(t))\) for all \(t\). Then the total signed curvature over one period is \(2\pi\): \(\int_0^{2\pi} \alpha'(t)\,dt = 2\pi\).

public theorem_wanted hopf_umlaufsatz
    {r : ℝ → Plane} {α : ℝ → ℝ}
    (_hr : IsPositiveSimpleClosedUnitSpeedCurve r)
    (_hα : IsTangentAngleLift r α) :
    totalCurvature α = 2 * Real.pi

Sources

• H. Hopf, Über die Drehung der Tangenten..., Compositio Math. 2 (1935). Knill, §170. Problem hopf_umlaufsatz of the lean-eval benchmark.

Uses 4

Statement usesPositively oriented simple closed unit-speed curve · Tangent-angle lift · Euclidean plane for the Umlaufsatz · Total signed curvature of a tangent-angle lift

9 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.