Fáry–Milnor theorem

AbbreviationEuclidean 3-space for the Fáry–Milnor theorem#✓fully proved

Euclidean 3-space is the real vector space \(\mathbb{R}^3\) with the Euclidean inner product and norm.

abbrev Space := EuclideanSpace ℝ (Fin 3)

Used by 8

Used byAcceleration of a space curve · Curvature of a space curve · Fáry–Milnor theorem · Smooth knot · Unknotted curve · Standard circle · Total curvature of a space curve · Velocity of a space curve

DefinitionPeriod of a parametrised knot#✓fully proved

The period used for parametrised knots is the real number \(2\pi\).

def period : ℝ := 2 * Real.pi

Used by 2

Used bySmooth knot · Total curvature of a space curve

DefinitionVelocity of a space curve#✓fully proved

For a curve \(r \colon \mathbb{R} \to \mathbb{R}^3\) and a real number \(t\), the velocity of \(r\) at \(t\) is its derivative \(r'(t)\), taken to be \(0\) when \(r\) is not differentiable at \(t\).

def velocity (r : ℝ → Space) (t : ℝ) : Space :=
  deriv r t

Uses 1 · Used by 4

Statement usesEuclidean 3-space for the Fáry–Milnor theorem

Used byAcceleration of a space curve · Curvature of a space curve · Smooth knot · Total curvature of a space curve

DefinitionAcceleration of a space curve#✓fully proved

For a curve \(r \colon \mathbb{R} \to \mathbb{R}^3\) and a real number \(t\), the acceleration of \(r\) at \(t\) is the derivative at \(t\) of its velocity \(s \mapsto r'(s)\), that is \(r''(t)\), where a derivative that does not exist is taken to be \(0\).

def acceleration (r : ℝ → Space) (t : ℝ) : Space :=
  deriv (velocity r) t

Uses 2 · Used by 1

Statement usesEuclidean 3-space for the Fáry–Milnor theorem · Velocity of a space curve

Used byCurvature of a space curve

DefinitionCurvature of a space curve#✓fully proved

For a curve \(r \colon \mathbb{R} \to \mathbb{R}^3\) with velocity \(r'\) and acceleration \(r''\), the curvature of \(r\) at a real number \(t\) is \(\kappa(t) = \lVert r'(t) \times r''(t) \rVert / \lVert r'(t) \rVert^3\), where \(\times\) is the cross product and \(\lVert \cdot \rVert\) is the Euclidean norm; the quotient is \(0\) when \(r'(t) = 0\).

def curvature (r : ℝ → Space) (t : ℝ) : ℝ :=
  ‖toLp 2 (crossProduct (ofLp (velocity r t)) (ofLp (acceleration r t)))‖ /
    ‖velocity r t‖ ^ 3

Uses 3 · Used by 1

Statement usesEuclidean 3-space for the Fáry–Milnor theorem · Acceleration of a space curve · Velocity of a space curve

Used byTotal curvature of a space curve

DefinitionTotal curvature of a space curve#✓fully proved

For a curve \(r \colon \mathbb{R} \to \mathbb{R}^3\) with velocity \(r'\) and curvature \(\kappa\), the total curvature of \(r\) is the arc-length integral \(\int_0^{2\pi} \kappa(t) \, \lVert r'(t) \rVert \, dt\) over one period, where the integral is taken to be \(0\) if the integrand is not integrable.

def totalCurvature (r : ℝ → Space) : ℝ :=
  ∫ t in (0 : ℝ)..period, curvature r t * ‖velocity r t‖

Uses 4 · Used by 1

Statement usesEuclidean 3-space for the Fáry–Milnor theorem · Curvature of a space curve · Period of a parametrised knot · Velocity of a space curve

Used byFáry–Milnor theorem

DefinitionStandard circle#✓fully proved

The standard circle is the curve \(\mathbb{R} \to \mathbb{R}^3\) given by \(t \mapsto (\cos t, \sin t, 0)\): the unit circle centred at the origin in the \(xy\)-plane.

def standardCircle (t : ℝ) : Space :=
  toLp 2 ![Real.cos t, Real.sin t, 0]

Uses 1 · Used by 1

Statement usesEuclidean 3-space for the Fáry–Milnor theorem

Used byUnknotted curve

StructureSmooth knot#✓fully proved

A curve \(r \colon \mathbb{R} \to \mathbb{R}^3\) is a smooth knot when it is real-analytic, periodic with period \(2\pi\), injective on \([0, 2\pi)\), and regular, that is, its velocity \(r'(t)\) is nonzero for every real number \(t\).

structure IsSmoothKnot (r : ℝ → Space) : Prop where
  smooth : ContDiff ℝ ⊤ r
  periodic : Function.Periodic r period
  injective_on_period : Set.InjOn r (Set.Ico (0 : ℝ) period)
  regular : ∀ t : ℝ, velocity r t ≠ 0

Uses 3 · Used by 2

Statement usesEuclidean 3-space for the Fáry–Milnor theorem · Period of a parametrised knot · Velocity of a space curve

Used byFáry–Milnor theorem · Unknotted curve

DefinitionUnknotted curve#✓fully proved

A curve \(r \colon \mathbb{R} \to \mathbb{R}^3\) is unknotted when there is a real-analytic map \(R \colon \mathbb{R} \times \mathbb{R} \to \mathbb{R}^3\) such that \(R(t, 0) = r(t)\) and \(R(t, 1) = (\cos t, \sin t, 0)\), the standard circle, for every real number \(t\), and for every \(s \in [0, 1]\) the curve \(t \mapsto R(t, s)\) is a smooth knot.

def IsUnknotted (r : ℝ → Space) : Prop :=
  ∃ R : ℝ → ℝ → Space,
    ContDiff ℝ ⊤ (fun p : ℝ × ℝ => R p.1 p.2) ∧
      (∀ t : ℝ, R t 0 = r t) ∧
      (∀ t : ℝ, R t 1 = standardCircle t) ∧
      ∀ s ∈ Set.Icc (0 : ℝ) 1, IsSmoothKnot (fun t : ℝ => R t s)

Uses 3 · Used by 1

Statement usesSmooth knot · Euclidean 3-space for the Fáry–Milnor theorem · Standard circle

Used byFáry–Milnor theorem

TheoremFáry–Milnor theorem#●ready to prove

Let \(r \colon \mathbb{R} \to \mathbb{R}^3\) be a smooth knot, that is, a real-analytic, \(2\pi\)-periodic curve that is injective on \([0, 2\pi)\) and has nonzero velocity everywhere. If the total curvature of \(r\) is at most \(4\pi\), then \(r\) is unknotted: there is a real-analytic isotopy from \(r\) to the standard circle through smooth knots.

public theorem_wanted fary_milnor_total_curvature
    {r : ℝ → Space} (_hknot : IsSmoothKnot r)
    (_hK : totalCurvature r ≤ 4 * Real.pi) :
    IsUnknotted r

Sources

• I. Fáry, 'Sur la courbure totale d'une courbe gauche faisant un nœud', Bull. Soc. Math. France 77 (1949) 128–138; J. Milnor, 'On the total curvature of knots', Ann. of Math. (2) 52 (1950) 248–257. §161 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem fary_milnor of the lean-eval benchmark.

Uses 4

Statement usesSmooth knot · Unknotted curve · Euclidean 3-space for the Fáry–Milnor theorem · Total curvature of a space curve

9 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.