Ropelength and crossing number

AbbreviationEuclidean 3-space#✓fully proved

The space \(\mathbb{R}^3\) with its Euclidean inner product and norm.

abbrev R3 : Type := EuclideanSpace ℝ (Fin 3)

Used by 52

Used byLinks with a crossing-free regular projection admit alternating diagrams · The crossing number is an isotopy invariant · A link's own regular projection bounds its crossing number · Height in the standard projection frame · Points with the same projection have different heights · The projected trace is the union of the projected components · Admitting an alternating diagram is an isotopy invariant · Standard projection to the plane · Point of a link at a parameter point · Projected curve of a link component · Projected tangent vector · Smooth ambient isotopy of Euclidean 3-space · Composition of ambient isotopies · Identity ambient isotopy · Isotopy of parametrized knots · Isotopy of parametrized links · Knots are the same as parametrized knots · Isotopy of knots agrees with isotopy of parametrized knots · Euclidean ambient isotopies as Conway-knot ambient isotopies · Parametrized knots as knots · Labeled two-component links as two-component links · Parametrized knot · Parametrized link · Ropelength is an isotopy invariant · Ropelength is at most the ropelength ratio · Inverse ambient isotopy · Conway-knot ambient isotopies as Euclidean ambient isotopies · Parametrized knot as a one-component link · Isotopic knots give isotopic one-component links · Knots as parametrized knots · Two-component links as labeled links · Total contour length of a parametrized link · Trace of a parametrized link · Two-component link isotopy agrees with labeled link isotopy · Extended circumradius of three points · Extended circumradius of a triangle · Collinear points have infinite extended circumradius · Equal first two points give infinite extended circumradius · Extended circumradius is invariant under reversal · Extended circumradius is symmetric in the first two points · Extended circumradius is symmetric in the last two points · Translation invariance of the extended circumradius · Contour length · Contour length of a \(C^1\) curve · Ropelength ratio · Thickness · Thickness is antitone · Thickness of the empty set · Thickness is at most every circumradius · Thickness of a single point · Triangle on three affinely independent points · Ordered triple of points

DefinitionOrdered triple of points#✓fully proved

For points \(p, q, r\) of Euclidean 3-space, the family indexed by \(\{0, 1, 2\}\) that sends \(0 \mapsto p\), \(1 \mapsto q\) and \(2 \mapsto r\).

def triplePoints (p q r : R3) : Fin 3 → R3 :=
  ![p, q, r]

Uses 1 · Used by 9

Statement usesEuclidean 3-space

Used byExtended circumradius of three points · Extended circumradius of a triangle · Collinear points have infinite extended circumradius · Equal first two points give infinite extended circumradius · Extended circumradius is invariant under reversal · Extended circumradius is symmetric in the first two points · Extended circumradius is symmetric in the last two points · Translation invariance of the extended circumradius · Triangle on three affinely independent points

DefinitionTriangle on three affinely independent points#✓fully proved

For points \(p, q, r\) of Euclidean 3-space whose ordered triple \((p, q, r)\) is affinely independent, the triangle in Euclidean 3-space with vertices \(p\), \(q\), \(r\), in that order.

def triangleOf (p q r : R3)
    (h : AffineIndependent ℝ (triplePoints p q r)) :
    Affine.Triangle ℝ R3 :=
  ⟨triplePoints p q r, h⟩

Uses 2 · Used by 8

Statement usesEuclidean 3-space · Ordered triple of points

Used byExtended circumradius of three points · Extended circumradius of a triangle · Collinear points have infinite extended circumradius · Equal first two points give infinite extended circumradius · Extended circumradius is invariant under reversal · Extended circumradius is symmetric in the first two points · Extended circumradius is symmetric in the last two points · Translation invariance of the extended circumradius

DefinitionExtended circumradius of three points#✓fully proved

For points \(p, q, r\) of Euclidean 3-space, the extended circumradius of \((p, q, r)\) is the following value in \([0, \infty]\). If \(p, q, r\) are affinely independent, it is the circumradius of the triangle with vertices \(p\), \(q\) and \(r\). Otherwise, that is, when the three points are collinear (in particular when two of them coincide), it is \(\infty\).

This matches the convention that collinear points determine a circle of infinite radius.

noncomputable def circumradiusENN (p q r : R3) : ENNReal :=
  if h : AffineIndependent ℝ (triplePoints p q r) then
    ENNReal.ofReal (triangleOf p q r h).circumradius
  else
    ⊤

Uses 3 · Used by 12

Statement usesEuclidean 3-space · Triangle on three affinely independent points · Ordered triple of points

Used byExtended circumradius of a triangle · Collinear points have infinite extended circumradius · Equal first two points give infinite extended circumradius · Extended circumradius is invariant under reversal · Extended circumradius is symmetric in the first two points · Extended circumradius is symmetric in the last two points · Translation invariance of the extended circumradius · Thickness · Thickness is antitone · Thickness of the empty set · Thickness is at most every circumradius · Thickness of a single point

TheoremExtended circumradius of a triangle#✓fully proved

Let \(p, q, r\) be points of Euclidean 3-space and let \(T\) be a triangle in Euclidean 3-space whose vertices, in order, are \(p\), \(q\) and \(r\). Then the extended circumradius of \((p, q, r)\) equals the circumradius of \(T\).

theorem circumradiusENN_eq_ofReal_circumradius {p q r : R3}
    (t : Affine.Triangle ℝ R3) (h0 : t.points 0 = p)
    (h1 : t.points 1 = q) (h2 : t.points 2 = r) :
    circumradiusENN p q r = ENNReal.ofReal t.circumradius

Uses 4

Statement usesEuclidean 3-space · Extended circumradius of three points

Proof usesTriangle on three affinely independent points · Ordered triple of points

TheoremCollinear points have infinite extended circumradius#✓fully proved

If \(p, q, r\) are points of Euclidean 3-space and the set \(\{p, q, r\}\) is collinear, then the extended circumradius of \((p, q, r)\) is \(\infty\).

theorem circumradiusENN_eq_top_of_collinear {p q r : R3}
    (h : Collinear ℝ ({p, q, r} : Set R3)) :
    circumradiusENN p q r = ⊤

Uses 4

Statement usesEuclidean 3-space · Extended circumradius of three points

Proof usesTriangle on three affinely independent points · Ordered triple of points

TheoremEqual first two points give infinite extended circumradius#✓fully proved

If \(p, q, r\) are points of Euclidean 3-space with \(p = q\), then the extended circumradius of \((p, q, r)\) is \(\infty\).

A triple with coincident points is treated as degenerate, not as having radius zero.

theorem circumradiusENN_eq_top_of_eq_left {p q r : R3} (h : p = q) :
    circumradiusENN p q r = ⊤

Uses 4 · Used by 1

Statement usesEuclidean 3-space · Extended circumradius of three points

Proof usesTriangle on three affinely independent points · Ordered triple of points

Used byThickness of a single point

TheoremExtended circumradius is symmetric in the first two points#✓fully proved

For all points \(p, q, r\) of Euclidean 3-space, the extended circumradius of \((q, p, r)\) equals the extended circumradius of \((p, q, r)\).

theorem circumradiusENN_swap_left (p q r : R3) :
    circumradiusENN q p r = circumradiusENN p q r

Uses 4

Statement usesEuclidean 3-space · Extended circumradius of three points

Proof usesTriangle on three affinely independent points · Ordered triple of points

TheoremExtended circumradius is symmetric in the last two points#✓fully proved

For all points \(p, q, r\) of Euclidean 3-space, the extended circumradius of \((p, r, q)\) equals the extended circumradius of \((p, q, r)\).

theorem circumradiusENN_swap_right (p q r : R3) :
    circumradiusENN p r q = circumradiusENN p q r

Uses 4

Statement usesEuclidean 3-space · Extended circumradius of three points

Proof usesTriangle on three affinely independent points · Ordered triple of points

TheoremExtended circumradius is invariant under reversal#✓fully proved

For all points \(p, q, r\) of Euclidean 3-space, the extended circumradius of \((r, q, p)\) equals the extended circumradius of \((p, q, r)\).

theorem circumradiusENN_reverse (p q r : R3) :
    circumradiusENN r q p = circumradiusENN p q r

Uses 4

Statement usesEuclidean 3-space · Extended circumradius of three points

Proof usesTriangle on three affinely independent points · Ordered triple of points

TheoremTranslation invariance of the extended circumradius#✓fully proved

For every vector \(v\) and all points \(p, q, r\) of Euclidean 3-space, the extended circumradius of \((v + p, v + q, v + r)\) equals the extended circumradius of \((p, q, r)\).

theorem circumradiusENN_vadd (v p q r : R3) :
    circumradiusENN (v +ᵥ p) (v +ᵥ q) (v +ᵥ r) =
      circumradiusENN p q r

Uses 4

Statement usesEuclidean 3-space · Extended circumradius of three points

Proof usesTriangle on three affinely independent points · Ordered triple of points

DefinitionThickness#✓fully proved

The thickness of a set \(s\) in Euclidean 3-space is the infimum, in \([0, \infty]\), of the extended circumradii of \((p, q, r)\) over all points \(p, q, r \in s\). Since the extended circumradius of three collinear points (in particular of three points two of which coincide) is \(\infty\), this is also the infimum over the triples of pairwise distinct points of \(s\).

noncomputable def thickness (s : Set R3) : ENNReal :=
  ⨅ p ∈ s, ⨅ q ∈ s, ⨅ r ∈ s, circumradiusENN p q r

Uses 2 · Used by 6

Statement usesEuclidean 3-space · Extended circumradius of three points

Used byRopelength ratio of a parametrized link · Ropelength ratio · Thickness is antitone · Thickness of the empty set · Thickness is at most every circumradius · Thickness of a single point

TheoremThickness is at most every circumradius#✓fully proved

For every set \(s\) in Euclidean 3-space and all points \(p, q, r \in s\), the thickness of \(s\) is at most the extended circumradius of \(p, q, r\).

theorem thickness_le {s : Set R3} {p q r : R3}
    (hp : p ∈ s) (hq : q ∈ s) (hr : r ∈ s) :
    thickness s ≤ circumradiusENN p q r

Uses 3

Statement usesEuclidean 3-space · Extended circumradius of three points · Thickness

TheoremThickness is antitone#✓fully proved

If \(s \subseteq t\) are sets in Euclidean 3-space, then the thickness of \(t\) is at most the thickness of \(s\): enlarging a set can only add triples and hence can only decrease the infimum.

theorem thickness_anti {s t : Set R3} (h : s ⊆ t) :
    thickness t ≤ thickness s

Uses 3

Statement usesEuclidean 3-space · Thickness

Proof usesExtended circumradius of three points

TheoremThickness of the empty set#✓fully proved

The empty subset of Euclidean 3-space has thickness \(\infty\), as an empty infimum in \([0, \infty]\).

@[simp]
theorem thickness_empty : thickness (∅ : Set R3) = ⊤

Uses 3

Statement usesEuclidean 3-space · Thickness

Proof usesExtended circumradius of three points

TheoremThickness of a single point#✓fully proved

For every point \(p\) of Euclidean 3-space, the set \(\{p\}\) has thickness \(\infty\): its only triple \((p, p, p)\) is degenerate.

theorem thickness_singleton (p : R3) : thickness {p} = ⊤

Uses 4

Statement usesEuclidean 3-space · Thickness

Proof usesExtended circumradius of three points · Equal first two points give infinite extended circumradius

DefinitionContour length#✓fully proved

Let \(\gamma\) be a map from \(\mathbb{R}\) to Euclidean 3-space and let \(a, b\) be real numbers. The contour length of \(\gamma\) on \([a, b]\) is the total variation of \(\gamma\) on \([a, b]\): the supremum, over all finite sequences \(t_0 \le t_1 \le \dots \le t_n\) of points of \([a, b]\), of \(\sum_{i < n} \lVert \gamma(t_{i+1}) - \gamma(t_i) \rVert\). It is a value in \([0, \infty]\).

For continuously differentiable curves it equals the integral of the speed.

noncomputable def contourLength (γ : ℝ → R3) (a b : ℝ) : ENNReal :=
  eVariationOn γ (Set.Icc a b)

Uses 1 · Used by 3

Statement usesEuclidean 3-space

Used byTotal contour length of a parametrized link · Contour length of a \(C^1\) curve · Ropelength ratio

TheoremContour length of a \(C^1\) curve#✓fully proved

Let \(a \le b\) be real numbers and let \(\gamma\) be a map from \(\mathbb{R}\) to Euclidean 3-space that is continuously differentiable on \([a, b]\). Then the contour length of \(\gamma\) on \([a, b]\) equals \(\int_a^b \lVert \gamma'(t) \rVert \, dt\).

theorem contourLength_eq_ofReal_integral_norm_deriv {γ : ℝ → R3}
    {a b : ℝ} (hab : a ≤ b) (hγ : ContDiffOn ℝ 1 γ (Set.Icc a b)) :
    contourLength γ a b =
      ENNReal.ofReal (∫ t in a..b, ‖deriv γ t‖)

Uses 3

Statement usesEuclidean 3-space · Contour length

Proof usesLength of a \(C^1\) curve

DefinitionRopelength ratio#✓fully proved

For a curve \(\gamma : \mathbb{R} \to \mathbb{R}^3\) and reals \(a, b\), the ropelength ratio of \(\gamma\) on \([a, b]\) is the contour length of \(\gamma\) on \([a, b]\) divided by the thickness of the trace \(\gamma([a, b])\). The quotient is taken in \([0, \infty]\), where \(c / 0 = \infty\) for \(c \ne 0\), \(0 / 0 = 0\) and \(c / \infty = 0\).

The ropelength of a knot or link type is a further infimum of this ratio over the curves representing the type.

noncomputable def ropelengthRatio (γ : ℝ → R3) (a b : ℝ) : ENNReal :=
  contourLength γ a b / thickness (γ '' Set.Icc a b)

Uses 3

Statement usesEuclidean 3-space · Contour length · Thickness

DefinitionAdmissible constants for the tight alternating knot inequality#✓fully proved

A real number \(c\) is admissible when \(c \ge 0\) and, for every \(n\) and every oriented labeled link type with \(n\) components that admits an alternating diagram and whose crossing number is a natural number \(k\), the ropelength of the type is at least \(c k\).

The restriction to finite crossing number excludes no such type: the alternating representative is itself a regular projection, so every link type admitting an alternating diagram has finite crossing number.

def IsAdmissibleAlternating (c : ℝ) : Prop :=
  0 ≤ c ∧ ∀ (n : ℕ) (L : ParametrizedLink n),
    L.AdmitsAlternatingDiagram → ∀ k : ℕ,
      L.crossingNumber = (k : ℕ∞) →
        ENNReal.ofReal c * (k : ENNReal) ≤ L.ropelength

Uses 4 · Used by 5

Statement usesParametrized link · Links admitting an alternating diagram · Crossing number of a link · Ropelength of a parametrized link

Used byZero is an admissible alternating constant · Admissible constants are at most the tight alternating knot constant · Admissible alternating constants are downward closed among nonnegative reals · Tight alternating knot constant · Upper bounds for the tight alternating knot constant

DefinitionTight alternating knot constant#✓fully proved

The tight alternating knot constant \(C_{22b} = b_0\) is the supremum, taken in the extended reals, of the set of real numbers \(c\) admissible for the tight alternating knot inequality: those \(c \ge 0\) such that every link type \(K\) that admits an alternating diagram and has finite crossing number \(\mathrm{Cr}(K)\) has ropelength \(\mathrm{L}(K) \ge c\,\mathrm{Cr}(K)\). The supremum is not assumed to be attained.

noncomputable def tightAlternatingKnotConstant : EReal :=
  sSup ((fun c : ℝ => (c : EReal)) '' {c : ℝ | IsAdmissibleAlternating c})

Uses 1 · Used by 3

Statement usesAdmissible constants for the tight alternating knot inequality

Used byAdmissible constants are at most the tight alternating knot constant · Upper bounds for the tight alternating knot constant · The tight alternating knot constant is nonnegative

TheoremZero is an admissible alternating constant#✓fully proved

The constant \(c = 0\) is admissible for the tight alternating knot inequality.

theorem isAdmissibleAlternating_zero : IsAdmissibleAlternating 0

Uses 5 · Used by 1

Statement usesAdmissible constants for the tight alternating knot inequality

Proof usesParametrized link · Links admitting an alternating diagram · Crossing number of a link · Ropelength of a parametrized link

Used byThe tight alternating knot constant is nonnegative

TheoremAdmissible alternating constants are downward closed among nonnegative reals#✓fully proved

Admissible alternating constants are downward closed among nonnegative reals. If a real number \(c\) is admissible for the tight alternating knot inequality and \(c'\) is a real number with \(0 \le c' \le c\), then \(c'\) is admissible as well.

theorem IsAdmissibleAlternating.of_le {c c' : ℝ}
    (hc : IsAdmissibleAlternating c) (h0 : 0 ≤ c') (h : c' ≤ c) :
    IsAdmissibleAlternating c'

Uses 5

Statement usesAdmissible constants for the tight alternating knot inequality

Proof usesParametrized link · Links admitting an alternating diagram · Crossing number of a link · Ropelength of a parametrized link

TheoremAdmissible constants are at most the tight alternating knot constant#✓fully proved

Admissible constants are at most the tight alternating knot constant. Every real number \(c\) that is admissible for the tight alternating knot inequality is at most the tight alternating knot constant.

theorem le_tightAlternatingKnotConstant {c : ℝ}
    (hc : IsAdmissibleAlternating c) :
    (c : EReal) ≤ tightAlternatingKnotConstant

Uses 2 · Used by 2

Statement usesAdmissible constants for the tight alternating knot inequality · Tight alternating knot constant

Used byUpper bounds for the tight alternating knot constant · The tight alternating knot constant is nonnegative

TheoremThe tight alternating knot constant is nonnegative#✓fully proved

The tight alternating knot constant, an extended real number, is at least \(0\).

theorem zero_le_tightAlternatingKnotConstant :
    (0 : EReal) ≤ tightAlternatingKnotConstant

Uses 3

Statement usesTight alternating knot constant

Proof usesZero is an admissible alternating constant · Admissible constants are at most the tight alternating knot constant

TheoremUpper bounds for the tight alternating knot constant#✓fully proved

For every extended real number \(b\), the tight alternating knot constant is at most \(b\) if and only if every real number \(c\) that is admissible for the tight alternating knot inequality satisfies \(c \le b\).

theorem tightAlternatingKnotConstant_le_iff {b : EReal} :
    tightAlternatingKnotConstant ≤ b ↔
      ∀ c : ℝ, IsAdmissibleAlternating c → (c : EReal) ≤ b

Uses 3

Statement usesAdmissible constants for the tight alternating knot inequality · Tight alternating knot constant

Proof usesAdmissible constants are at most the tight alternating knot constant

TheoremAlternating link types have finite crossing number#✓fully proved

If an oriented labeled link type with \(n\) components admits an alternating diagram, then its crossing number is finite: the alternating representative is itself a regular projection.

theorem crossingNumber_lt_top_of_admitsAlternatingDiagram {n : ℕ}
    {L : ParametrizedLink n} (hL : L.AdmitsAlternatingDiagram) :
    L.crossingNumber < ⊤

Uses 7 · Used by 1

Statement usesParametrized link · Links admitting an alternating diagram · Crossing number of a link

Proof usesAlternating regular projections · Regular projections · Isotopy of parametrized links · Finiteness of the crossing number

Used byAlternating link types have a natural-number crossing number

TheoremAlternating link types have a natural-number crossing number#✓fully proved

If an oriented labeled link type with \(n\) components admits an alternating diagram, then its crossing number equals some natural number \(k\).

theorem exists_crossingNumber_eq_natCast_of_admitsAlternatingDiagram
    {n : ℕ} {L : ParametrizedLink n}
    (hL : L.AdmitsAlternatingDiagram) :
    ∃ k : ℕ, L.crossingNumber = (k : ℕ∞)

Uses 4

Statement usesParametrized link · Links admitting an alternating diagram · Crossing number of a link

Proof usesAlternating link types have finite crossing number

DefinitionAdmissible constants for the tight-knot inequality#✓fully proved

A real number \(c\) is admissible for the tight-knot inequality when \(c \ge 0\) and, for every \(n \in \mathbb{N}\), every parametrized link \(L\) with \(n\) components and every \(k \in \mathbb{N}\) such that the crossing number of \(L\) equals \(k\), the ropelength of \(L\) is at least \(c \, k^{3/4}\), the inequality being read in \([0, \infty]\). Here the crossing number and the ropelength of \(L\) are those of its oriented labeled ambient-isotopy type.

Link types of infinite crossing number, that is, types none of whose representatives admits a regular projection, impose no constraint.

def IsAdmissible (c : ℝ) : Prop :=
  0 ≤ c ∧ ∀ (n : ℕ) (L : ParametrizedLink n) (k : ℕ),
    L.crossingNumber = (k : ℕ∞) →
      ENNReal.ofReal c * ENNReal.ofReal ((k : ℝ) ^ (3 / 4 : ℝ)) ≤
        L.ropelength

Uses 3 · Used by 5

Statement usesParametrized link · Crossing number of a link · Ropelength of a parametrized link

Used byZero is an admissible tight-knot constant · Admissible constants are bounded by the tight knot constant · Admissibility passes to smaller nonnegative constants · Tight knot constant · Upper bounds for the tight knot constant

DefinitionTight knot constant#✓fully proved

The tight knot constant \(C_{22a}\) is the supremum, taken in the extended reals \([-\infty, \infty]\), of the set of real numbers \(c\) that are admissible for the tight-knot inequality \(\mathrm{ropelength} \ge c \cdot (\text{crossing number})^{3/4}\) on link types. The supremum is not assumed to be attained.

noncomputable def tightKnotConstant : EReal :=
  sSup ((fun c : ℝ => (c : EReal)) '' {c : ℝ | IsAdmissible c})

Uses 1 · Used by 3

Statement usesAdmissible constants for the tight-knot inequality

Used byAdmissible constants are bounded by the tight knot constant · Upper bounds for the tight knot constant · The tight knot constant is nonnegative

TheoremZero is an admissible tight-knot constant#✓fully proved

The real number \(0\) is admissible for the tight-knot inequality between the ropelength and the crossing number of link types.

theorem isAdmissible_zero : IsAdmissible 0

Uses 4 · Used by 1

Statement usesAdmissible constants for the tight-knot inequality

Proof usesParametrized link · Crossing number of a link · Ropelength of a parametrized link

Used byThe tight knot constant is nonnegative

TheoremAdmissibility passes to smaller nonnegative constants#✓fully proved

If a real number \(c\) is admissible for the tight-knot inequality and \(c'\) is a real number with \(0 \le c' \le c\), then \(c'\) is admissible for the tight-knot inequality as well.

theorem IsAdmissible.of_le {c c' : ℝ} (hc : IsAdmissible c)
    (h0 : 0 ≤ c') (h : c' ≤ c) : IsAdmissible c'

Uses 4

Statement usesAdmissible constants for the tight-knot inequality

Proof usesParametrized link · Crossing number of a link · Ropelength of a parametrized link

TheoremAdmissible constants are bounded by the tight knot constant#✓fully proved

Let \(C_{22a}\) be the tight knot constant. Every real number \(c\) that is admissible for the tight-knot inequality satisfies \(c \le C_{22a}\) in the extended reals.

theorem le_tightKnotConstant {c : ℝ} (hc : IsAdmissible c) :
    (c : EReal) ≤ tightKnotConstant

Uses 2 · Used by 2

Statement usesAdmissible constants for the tight-knot inequality · Tight knot constant

Used byUpper bounds for the tight knot constant · The tight knot constant is nonnegative

TheoremThe tight knot constant is nonnegative#✓fully proved

The tight knot constant \(C_{22a}\) satisfies \(0 \le C_{22a}\) in the extended reals.

theorem zero_le_tightKnotConstant : (0 : EReal) ≤ tightKnotConstant

Uses 3

Statement usesTight knot constant

Proof usesZero is an admissible tight-knot constant · Admissible constants are bounded by the tight knot constant

TheoremUpper bounds for the tight knot constant#✓fully proved

For every extended real number \(b\), the tight knot constant \(C_{22a}\) satisfies \(C_{22a} \le b\) if and only if every real number \(c\) that is admissible for the tight-knot inequality satisfies \(c \le b\).

This is the characteristic rule for proving upper bounds on the tight knot constant without unfolding its definition as a supremum.

theorem tightKnotConstant_le_iff {b : EReal} :
    tightKnotConstant ≤ b ↔
      ∀ c : ℝ, IsAdmissible c → (c : EReal) ≤ b

Uses 3

Statement usesAdmissible constants for the tight-knot inequality · Tight knot constant

Proof usesAdmissible constants are bounded by the tight knot constant

35 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.