Moser's worm problem

AbbreviationParameter interval of unit arcs#✓fully proved

Planar arcs are parametrized by the closed unit interval \([0, 1]\) of real numbers.

abbrev ArcParameter := Set.Icc (0 : ℝ) 1
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Used by 8
Used byThe closed unit disk covers every unit arc · Sets that cover every unit arc · Sets covering every unit arc are nonempty · The identity on the unit interval has total variation one · Straight path · The straight segment has length one · Straight unit arc · Unit arc

StructureUnit arc#✓fully proved

A unit arc is a continuous map \(\gamma\) from the closed interval \([0, 1]\) to the complex plane whose length, the total variation of \(\gamma\) on \([0, 1]\), equals \(1\).

structure UnitArc where
  path : C(ArcParameter, ℂ)
  length_eq_one : eVariationOn path Set.univ = 1
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 4
Statement usesParameter interval of unit arcs
Used byThe closed unit disk covers every unit arc · Sets that cover every unit arc · Sets covering every unit arc are nonempty · Straight unit arc

DefinitionDirect rigid motion of the plane#✓fully proved

For a real angle \(\theta\) and a complex number \(\tau\), the motion with angle \(\theta\) and translation \(\tau\) sends \(z \in \mathbb{C}\) to \(e^{i\theta} z + \tau\): a rotation about the origin by \(\theta\) followed by translation by \(\tau\), with neither reflection nor rescaling.

noncomputable def move (angle : ℝ) (translation z : ℂ) : ℂ :=
  Complex.exp (angle * Complex.I) * z + translation
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Used by 4
Used byThe closed unit disk covers every unit arc · Sets that cover every unit arc · Direct rigid motions of the plane are isometries · Sets covering every unit arc are nonempty

TheoremDirect rigid motions of the plane are isometries#✓fully proved

For every real angle \(\theta\) and every complex number \(\tau\), the map \(z \mapsto e^{i\theta} z + \tau\) of the complex plane is an isometry: it preserves the distance \(|z - w|\) between any two points \(z, w \in \mathbb{C}\).

theorem move_isometry (angle : ℝ) (translation : ℂ) : Isometry (move angle translation)
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1
Statement usesDirect rigid motion of the plane

DefinitionStraight path#✓fully proved

The straight path is the continuous map from the interval \([0, 1]\) to the complex plane that sends each \(t \in [0, 1]\) to \(t\) viewed as a complex number; it traces the segment from \(0\) to \(1\).

noncomputable def straightPath : C(ArcParameter, ℂ) :=
  ⟨fun t => (t.1 : ℂ), Complex.continuous_ofReal.comp continuous_subtype_val⟩
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 2
Statement usesParameter interval of unit arcs
Used byThe straight segment has length one · Straight unit arc

TheoremThe identity on the unit interval has total variation one#✓fully proved

The total variation of the inclusion \([0, 1] \to \mathbb{R}\), \(t \mapsto t\), over the whole interval \([0, 1]\) equals \(1\).

theorem parameter_variation :
    eVariationOn (Subtype.val : ArcParameter → ℝ) Set.univ = 1
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesParameter interval of unit arcs
Used byThe straight segment has length one

TheoremThe straight segment has length one#✓fully proved

The path \([0, 1] \to \mathbb{C}\), \(t \mapsto t\), which traces the segment from \(0\) to \(1\) on the real axis, has total variation (length) exactly \(1\) over \([0, 1]\).

theorem straightPath_length : eVariationOn straightPath Set.univ = 1
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 3 · Used by 1
Statement usesParameter interval of unit arcs · Straight path
Proof usesThe identity on the unit interval has total variation one
Used byStraight unit arc

DefinitionStraight unit arc#✓fully proved

The straight unit arc is the unit arc whose curve is the straight path \(t \mapsto t\) from \([0, 1]\) to the complex plane, which traces the segment from \(0\) to \(1\) and has length \(1\).

noncomputable def straightUnitArc : UnitArc := ⟨straightPath, straightPath_length⟩
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 4 · Used by 1
Statement usesParameter interval of unit arcs · Unit arc · Straight path · The straight segment has length one
Used bySets covering every unit arc are nonempty

DefinitionSets that cover every unit arc#✓fully proved

A set \(\Omega \subseteq \mathbb{C}\) covers every unit arc when for every unit arc \(\gamma : [0, 1] \to \mathbb{C}\), that is, every continuous map whose total variation (length) is exactly \(1\), there are an angle \(\theta \in \mathbb{R}\) and a translation \(\tau \in \mathbb{C}\) such that \(e^{i\theta} \gamma(t) + \tau \in \Omega\) for every \(t \in [0, 1]\).

Only rotations followed by translations are allowed; reflections and rescalings are not.

def CoversEveryUnitArc (Ω : Set ℂ) : Prop :=
  ∀ arc : UnitArc, ∃ angle : ℝ, ∃ translation : ℂ,
    ∀ t : ArcParameter, move angle translation (arc.path t) ∈ Ω
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 3 · Used by 11
Statement usesParameter interval of unit arcs · Unit arc · Direct rigid motion of the plane
Used byThe closed unit disk covers every unit arc · The closed unit disk is a convex universal cover · The empty set does not cover every unit arc · The disk of diameter one covers every unit arc (claim) · The half-disk of diameter one covers every unit arc (claim) · Convex universal covers · Universal covers · Convex universal covers are universal covers · Sets covering every unit arc are nonempty · Convex universal covers are null-measurable · Wetzel's sector covering claim

TheoremSets covering every unit arc are nonempty#✓fully proved

If a set \(\Omega \subseteq \mathbb{C}\) covers every unit arc, that is, contains a rotated and translated copy of every continuous curve \([0, 1] \to \mathbb{C}\) of length exactly one, then \(\Omega\) is nonempty.

theorem CoversEveryUnitArc.nonempty {Ω : Set ℂ} (h : CoversEveryUnitArc Ω) : Ω.Nonempty
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 5 · Used by 1
Statement usesSets that cover every unit arc
Proof usesParameter interval of unit arcs · Unit arc · Direct rigid motion of the plane · Straight unit arc
Used byThe empty set does not cover every unit arc

TheoremThe empty set does not cover every unit arc#✓fully proved

The empty set \(\emptyset \subseteq \mathbb{C}\) does not cover every unit arc: not every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be mapped into \(\emptyset\) by a rotation followed by a translation.

theorem empty_not_covers : ¬ CoversEveryUnitArc (∅ : Set ℂ)
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 2
Statement usesSets that cover every unit arc
Proof usesSets covering every unit arc are nonempty

DefinitionConvex universal covers#✓fully proved

A set \(\Omega \subseteq \mathbb{C}\) is a convex universal cover when it is nonempty, convex (as a subset of the real plane \(\mathbb{C} \cong \mathbb{R}^2\)), and covers every unit arc: for every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) there are \(\theta \in \mathbb{R}\) and \(\tau \in \mathbb{C}\) with \(e^{i\theta} \gamma(t) + \tau \in \Omega\) for all \(t \in [0, 1]\).

def IsConvexUniversalCover (Ω : Set ℂ) : Prop :=
  Ω.Nonempty ∧ Convex ℝ Ω ∧ CoversEveryUnitArc Ω
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 8
Statement usesSets that cover every unit arc
Used byThe closed unit disk is a convex universal cover · The infimal area of convex universal covers is finite · Areas of convex universal covers · The set of convex cover areas is nonempty · Convex universal covers are universal covers · The minimal-convex-cover claim · The nonconvex worm cover constant is at most the convex one · Convex universal covers are null-measurable

DefinitionUniversal covers#✓fully proved

A set \(\Omega \subseteq \mathbb{C}\) is a universal cover when it is nonempty and covers every unit arc: for every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) there are \(\theta \in \mathbb{R}\) and \(\tau \in \mathbb{C}\) with \(e^{i\theta} \gamma(t) + \tau \in \Omega\) for all \(t \in [0, 1]\). Neither convexity nor measurability of \(\Omega\) is required.

def IsUniversalCover (Ω : Set ℂ) : Prop :=
  Ω.Nonempty ∧ CoversEveryUnitArc Ω
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 8
Statement usesSets that cover every unit arc
Used byThe infimal area of universal covers is finite · Areas of universal covers · The set of universal cover areas is nonempty · Convex universal covers are universal covers · The Norwood–Poole cover claim · The Ploymaklam–Wichiramala cover claim · The nonconvex worm cover constant is at most the convex one · Covers give upper bounds on the nonconvex worm cover constant

TheoremConvex universal covers are null-measurable#✓fully proved

If \(\Omega \subseteq \mathbb{C}\) is a convex universal cover of unit arcs, then \(\Omega\) is a null-measurable set for Lebesgue measure on \(\mathbb{C}\).

theorem IsConvexUniversalCover.nullMeasurableSet {Ω : Set ℂ}
    (h : IsConvexUniversalCover Ω) : NullMeasurableSet Ω volume
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 2
Statement usesConvex universal covers
Proof usesSets that cover every unit arc

TheoremConvex universal covers are universal covers#✓fully proved

Every convex universal cover \(\Omega \subseteq \mathbb{C}\) is a universal cover.

theorem IsConvexUniversalCover.isUniversalCover {Ω : Set ℂ}
    (h : IsConvexUniversalCover Ω) : IsUniversalCover Ω
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 3 · Used by 3
Statement usesConvex universal covers · Universal covers
Proof usesSets that cover every unit arc
Used byThe infimal area of universal covers is finite · The set of universal cover areas is nonempty · The nonconvex worm cover constant is at most the convex one

DefinitionAreas of convex universal covers#✓fully proved

The set of convex cover areas is the set of all values \(\operatorname{vol}(\Omega) \in [0, \infty]\), where \(\Omega \subseteq \mathbb{C}\) ranges over the convex universal covers and \(\operatorname{vol}\) is Lebesgue measure on \(\mathbb{C} \cong \mathbb{R}^2\).

noncomputable def convexCoverAreas : Set ENNReal :=
  {a | ∃ Ω : Set ℂ, IsConvexUniversalCover Ω ∧ volume Ω = a}
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 4
Statement usesConvex universal covers
Used byInfimal area of convex universal covers · The infimal area of convex universal covers is finite · The set of convex cover areas is nonempty · The nonconvex worm cover constant is at most the convex one

DefinitionAreas of universal covers#✓fully proved

The set of values \(\lambda(\Omega) \in [0, \infty]\), where \(\Omega \subseteq \mathbb{C}\) ranges over the universal covers and \(\lambda\) is Lebesgue measure on \(\mathbb{C} \cong \mathbb{R}^2\), applied as an outer measure since \(\Omega\) need not be measurable.

noncomputable def coverAreas : Set ENNReal :=
  {a | ∃ Ω : Set ℂ, IsUniversalCover Ω ∧ volume Ω = a}
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 5
Statement usesUniversal covers
Used byInfimal area of a universal cover · The infimal area of universal covers is finite · The set of universal cover areas is nonempty · The nonconvex worm cover constant is at most the convex one · Covers give upper bounds on the nonconvex worm cover constant

DefinitionInfimal area of convex universal covers#✓fully proved

The convex cover area infimum is the infimum in \([0, \infty]\) of the set of convex cover areas, that is, the infimum of the Lebesgue areas of all convex universal covers \(\Omega \subseteq \mathbb{C}\).

noncomputable def convexCoverAreaInfimum : ENNReal := sInf convexCoverAreas
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 4
Statement usesAreas of convex universal covers
Used byThe infimal area of convex universal covers is finite · Moser's convex worm cover constant · The convex worm cover constant is nonnegative · The nonconvex worm cover constant is at most the convex one

DefinitionInfimal area of a universal cover#✓fully proved

The infimum in \([0, \infty]\) of the areas \(\lambda(\Omega)\) of the universal covers \(\Omega \subseteq \mathbb{C}\), where \(\lambda\) is Lebesgue measure on \(\mathbb{C} \cong \mathbb{R}^2\), applied as an outer measure since \(\Omega\) need not be measurable.

noncomputable def coverAreaInfimum : ENNReal := sInf coverAreas
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 5
Statement usesAreas of universal covers
Used byThe infimal area of universal covers is finite · The nonconvex worm cover constant is at most the convex one · Covers give upper bounds on the nonconvex worm cover constant · Nonconvex worm cover constant · Nonnegativity of the nonconvex worm cover constant

TheoremThe closed unit disk covers every unit arc#✓fully proved

For every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) there are an angle \(\theta \in \mathbb{R}\) and a translation \(c \in \mathbb{C}\) such that \(|e^{i\theta}\gamma(t) + c| \le 1\) for every \(t \in [0, 1]\); that is, the closed disk of radius \(1\) centred at \(0\) covers every unit arc.

theorem closedBall_one_covers : CoversEveryUnitArc (Metric.closedBall (0 : ℂ) 1)
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 4 · Used by 1
Statement usesSets that cover every unit arc
Proof usesParameter interval of unit arcs · Unit arc · Direct rigid motion of the plane
Used byThe closed unit disk is a convex universal cover

TheoremThe closed unit disk is a convex universal cover#✓fully proved

The closed disk \(\{z \in \mathbb{C} : |z| \le 1\}\) is a convex universal cover: it is nonempty, convex, and covers every unit arc.

theorem closedBall_one_isConvexUniversalCover :
    IsConvexUniversalCover (Metric.closedBall (0 : ℂ) 1)
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 3 · Used by 4
Statement usesConvex universal covers
Proof usesSets that cover every unit arc · The closed unit disk covers every unit arc
Used byThe infimal area of convex universal covers is finite · The set of convex cover areas is nonempty · The infimal area of universal covers is finite · The set of universal cover areas is nonempty

TheoremThe set of convex cover areas is nonempty#✓fully proved

The set of convex cover areas, the Lebesgue areas of all convex universal covers in \(\mathbb{C}\), is nonempty; that is, some convex universal cover exists.

theorem convexCoverAreas_nonempty : convexCoverAreas.Nonempty
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 3
Statement usesAreas of convex universal covers
Proof usesConvex universal covers · The closed unit disk is a convex universal cover

TheoremThe set of universal cover areas is nonempty#✓fully proved

The set of values \(\lambda(\Omega) \in [0, \infty]\), where \(\Omega \subseteq \mathbb{C}\) ranges over the universal covers and \(\lambda\) is Lebesgue outer measure on \(\mathbb{C} \cong \mathbb{R}^2\), is nonempty.

theorem coverAreas_nonempty : coverAreas.Nonempty
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 4
Statement usesAreas of universal covers
Proof usesConvex universal covers are universal covers · Universal covers · The closed unit disk is a convex universal cover

TheoremThe infimal area of convex universal covers is finite#✓fully proved

The convex cover area infimum, the infimum in \([0, \infty]\) of the Lebesgue areas of all convex universal covers in \(\mathbb{C}\), is not \(\infty\).

theorem convexCoverAreaInfimum_ne_top : convexCoverAreaInfimum ≠ ⊤
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 4 · Used by 1
Statement usesInfimal area of convex universal covers
Proof usesConvex universal covers · The closed unit disk is a convex universal cover · Areas of convex universal covers
Used byThe nonconvex worm cover constant is at most the convex one

TheoremThe infimal area of universal covers is finite#✓fully proved

The cover area infimum, the infimum in \([0, \infty]\) of the Lebesgue areas of all universal covers in \(\mathbb{C}\) (nonempty sets that cover every unit arc, not necessarily convex), is not \(\infty\).

theorem coverAreaInfimum_ne_top : coverAreaInfimum ≠ ⊤
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 5 · Used by 1
Statement usesInfimal area of a universal cover
Proof usesConvex universal covers are universal covers · Universal covers · The closed unit disk is a convex universal cover · Areas of universal covers
Used byThe nonconvex worm cover constant is at most the convex one

DefinitionMoser's convex worm cover constant#✓fully proved

The convex worm cover constant is the real number obtained from the convex cover area infimum, the infimum in \([0, \infty]\) of the Lebesgue areas of all convex universal covers in \(\mathbb{C}\), by the conversion \([0, \infty] \to \mathbb{R}\) that is the identity on finite values and sends \(\infty\) to \(0\).

That infimum is finite, so the constant equals the infimal area itself.

noncomputable def convexWormCoverConstant : ℝ := convexCoverAreaInfimum.toReal
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 14
Statement usesInfimal area of convex universal covers
Used byThe convex worm cover constant is nonnegative · Khandhawit–Pagonakis–Sriswasdi 2013 lower bound on the convex worm cover constant (claim) · Khandhawit–Sriswasdi 2009 lower bound for the convex worm cover constant (claim) · Wetzel's 1973 lower bound for the convex worm cover constant (claim) · The minimal-convex-cover claim · The nonconvex worm cover constant is at most the convex one · Statement of the Gerriets–Poole upper bound \(0.2861\) for convex worm covers · Statement of Gerriets' upper bound \(0.3214\) for convex worm covers · Statement of the Norwood–Poole–Laidacker upper bound \(0.27524\) for convex worm covers · Proposition: the convex worm cover constant is at most π/8 · Proposition: the convex worm cover constant is at most π/4 · Proposition: the convex worm cover constant is at most π/12 · Proposition: the convex worm cover constant is at most 0.270911861 · Proposition: the convex worm cover constant is at most 0.34501

DefinitionNonconvex worm cover constant#✓fully proved

The nonconvex worm cover constant is the real number obtained from the cover area infimum, the infimum in \([0, \infty]\) of the Lebesgue outer measures of all universal covers of unit arcs (nonempty sets \(\Omega \subseteq \mathbb{C}\) containing a rotated and translated copy of every continuous curve of length one), by converting it to a real number. The conversion would send \(\infty\) to \(0\), but this infimum is finite.

noncomputable def nonconvexWormCoverConstant : ℝ := coverAreaInfimum.toReal
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 6
Statement usesInfimal area of a universal cover
Used byThe nonconvex worm cover constant is at most the convex one · The positivity claim for the nonconvex worm cover constant · Statement of the Norwood–Poole upper bound \(0.260437\) for worm covers · Covers give upper bounds on the nonconvex worm cover constant · Statement of the Ploymaklam–Wichiramala upper bound \(0.26007\) for worm covers · Nonnegativity of the nonconvex worm cover constant

TheoremThe convex worm cover constant is nonnegative#✓fully proved

The convex worm cover constant is at least \(0\).

theorem convexWormCoverConstant_nonneg : 0 ≤ convexWormCoverConstant
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 2
Statement usesMoser's convex worm cover constant
Proof usesInfimal area of convex universal covers

TheoremNonnegativity of the nonconvex worm cover constant#✓fully proved

The nonconvex worm cover constant is greater than or equal to \(0\).

theorem nonconvexWormCoverConstant_nonneg : 0 ≤ nonconvexWormCoverConstant
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 2
Statement usesNonconvex worm cover constant
Proof usesInfimal area of a universal cover

TheoremThe nonconvex worm cover constant is at most the convex one#✓fully proved

The nonconvex worm cover constant (the infimal area of universal covers of unit arcs) is less than or equal to the convex worm cover constant (the infimal area of convex universal covers of unit arcs).

theorem nonconvex_le_convex : nonconvexWormCoverConstant ≤ convexWormCoverConstant
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 11
Statement usesMoser's convex worm cover constant · Nonconvex worm cover constant
Proof usesConvex universal covers · Convex universal covers are universal covers · Universal covers · Infimal area of convex universal covers · The infimal area of convex universal covers is finite · Areas of convex universal covers · Infimal area of a universal cover · The infimal area of universal covers is finite · Areas of universal covers

DefinitionDisk of radius one half#✓fully proved

The closed disk \(\{z \in \mathbb{C} : |z| \le 1/2\}\) of radius \(1/2\) centred at \(0\).

noncomputable def halfDisk : Set ℂ :=
  {z | ‖z‖ ≤ (1 : ℝ) / 2}
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Used by 1
Used byThe disk of diameter one covers every unit arc (claim)

DefinitionSemidisk of radius one half#✓fully proved

The closed upper half-disk \(\{z \in \mathbb{C} : |z| \le 1/2,\ \operatorname{Im} z \ge 0\}\) of radius \(1/2\) centred at \(0\).

noncomputable def halfSemidisk : Set ℂ :=
  {z | ‖z‖ ≤ (1 : ℝ) / 2 ∧ 0 ≤ z.im}
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Used by 1
Used byThe half-disk of diameter one covers every unit arc (claim)

DefinitionWetzel's sector#✓fully proved

This is the closed circular sector of radius \(1\) and opening angle \(30^\circ\) with apex at the origin, placed symmetrically about the positive real axis: the set of complex numbers \(z\) with \(|z| \le 1\), \(\operatorname{Re} z \ge 0\) and \(|\operatorname{Im} z| \le \tan(\pi/12) \operatorname{Re} z\).

noncomputable def wetzelSector : Set ℂ :=
  {z | ‖z‖ ≤ 1 ∧ 0 ≤ z.re ∧ |z.im| ≤ Real.tan (Real.pi / 12) * z.re}
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Used by 1
Used byWetzel's sector covering claim

TheoremCovers give upper bounds on the nonconvex worm cover constant#✓fully proved

Let \(r \ge 0\) be a real number. If some set \(\Omega \subseteq \mathbb{C}\) is a universal cover of unit arcs whose Lebesgue outer measure is at most \(r\), then the nonconvex worm cover constant is at most \(r\).

theorem nonconvexUpperBound_of_cover {r : ℝ} (hr : 0 ≤ r)
    (h : ∃ Ω : Set ℂ, IsUniversalCover Ω ∧ volume Ω ≤ ENNReal.ofReal r) :
    nonconvexWormCoverConstant ≤ r
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 4 · Used by 2
Statement usesUniversal covers · Nonconvex worm cover constant
Proof usesInfimal area of a universal cover · Areas of universal covers
Used byA Norwood–Poole cover bounds the nonconvex worm cover constant · Covers of area at most \(0.26007\) bound the nonconvex worm cover constant

DefinitionProposition: the convex worm cover constant is at most π/4#✓fully proved

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant is the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation. This proposition states that the convex worm cover constant is at most \(\pi/4\).

def upperBoundPiOverFour : Prop := convexWormCoverConstant ≤ Real.pi / 4
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byThe convex worm cover constant is at most π/4

DefinitionProposition: the convex worm cover constant is at most π/8#✓fully proved

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant is the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation. This proposition states that the convex worm cover constant is at most \(\pi/8\).

def upperBoundPiOverEight : Prop := convexWormCoverConstant ≤ Real.pi / 8
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byThe convex worm cover constant is at most π/8

DefinitionProposition: the convex worm cover constant is at most 0.34501#✓fully proved

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant is the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation. This proposition states that the convex worm cover constant is at most \(0.34501\).

def upperBoundWetzel1973 : Prop := convexWormCoverConstant ≤ (34501 : ℝ) / 100000
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byThe convex worm cover constant is at most 0.34501

DefinitionStatement of Gerriets' upper bound \(0.3214\) for convex worm covers#✓fully proved

The proposition that Moser's convex worm cover constant, the infimum of the areas of convex planar sets containing a rotated and translated copy of every planar curve of length \(1\), is at most \(0.3214\).

def upperBoundGerriets1972 : Prop := convexWormCoverConstant ≤ (3214 : ℝ) / 10000
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byGerriets' upper bound for the convex worm cover constant

DefinitionStatement of the Gerriets–Poole upper bound \(0.2861\) for convex worm covers#✓fully proved

The proposition that Moser's convex worm cover constant, the infimum of the areas of convex planar sets containing a rotated and translated copy of every planar curve of length \(1\), is at most \(0.2861\).

def upperBoundGerrietsPoole1974 : Prop := convexWormCoverConstant ≤ (28610 : ℝ) / 100000
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byGerriets–Poole upper bound for the convex worm cover constant

DefinitionStatement of the Norwood–Poole–Laidacker upper bound \(0.27524\) for convex worm covers#✓fully proved

The proposition that Moser's convex worm cover constant, the infimum of the areas of convex planar sets containing a rotated and translated copy of every planar curve of length \(1\), is at most \(0.27524\).

def upperBoundNorwoodPooleLaidacker1992 : Prop :=
  convexWormCoverConstant ≤ (27524 : ℝ) / 100000
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byNorwood–Poole–Laidacker upper bound for the convex worm cover constant

DefinitionProposition: the convex worm cover constant is at most 0.270911861#✓fully proved

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant is the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation. This proposition states that the convex worm cover constant is at most \(0.270911861\).

def upperBoundWang2006 : Prop := convexWormCoverConstant ≤ (270911861 : ℝ) / 1000000000
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byThe convex worm cover constant is at most 0.270911861

DefinitionProposition: the convex worm cover constant is at most π/12#✓fully proved

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant is the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation. This proposition states that the convex worm cover constant is at most \(\pi/12\).

def upperBoundPiOverTwelve : Prop := convexWormCoverConstant ≤ Real.pi / 12
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byThe convex worm cover constant is at most π/12

DefinitionWetzel's 1973 lower bound for the convex worm cover constant (claim)#✓fully proved

This proposition asserts that \(0.2194 \le \mu\), where \(\mu\) is the convex worm cover constant: the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) such that every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by a rotation followed by a translation.

def lowerBoundWetzel1973 : Prop := (2194 : ℝ) / 10000 ≤ convexWormCoverConstant
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byWetzel's 1973 lower bound for the convex worm cover constant

DefinitionKhandhawit–Sriswasdi 2009 lower bound for the convex worm cover constant (claim)#✓fully proved

This proposition asserts that \(0.227498 \le \mu\), where \(\mu\) is the convex worm cover constant: the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) such that every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by a rotation followed by a translation.

def lowerBoundKhandhawitSriswasdi2009 : Prop :=
  (227498 : ℝ) / 1000000 ≤ convexWormCoverConstant
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byKhandhawit–Sriswasdi 2009 lower bound for the convex worm cover constant

DefinitionKhandhawit–Pagonakis–Sriswasdi 2013 lower bound on the convex worm cover constant (claim)#✓fully proved

This proposition asserts that \(0.232239 \le \mu\), where \(\mu\) is the convex worm cover constant: the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) such that every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by a rotation followed by a translation.

def lowerBoundKhandhawitPagonakisSriswasdi2013 : Prop :=
  (232239 : ℝ) / 1000000 ≤ convexWormCoverConstant
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesMoser's convex worm cover constant
Used byKhandhawit–Pagonakis–Sriswasdi 2013 lower bound on the convex worm cover constant

DefinitionThe minimal-convex-cover claim#✓fully proved

Call a nonempty convex set \(\Omega \subseteq \mathbb{C}\) a convex universal cover if every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation, and let the convex worm cover constant be the infimum of the areas (Lebesgue measures) of all convex universal covers, which is a finite real number. This is the proposition that some convex universal cover has area equal to the convex worm cover constant.

Attainment of the minimum is a claim to be proved; it is not built into the definition of the constant.

def minimalConvexCoverExists : Prop :=
  ∃ Ω : Set ℂ, IsConvexUniversalCover Ω ∧
    volume Ω = ENNReal.ofReal convexWormCoverConstant
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 2 · Used by 1
Statement usesConvex universal covers · Moser's convex worm cover constant
Used byA minimal convex cover for unit arcs exists

DefinitionThe Norwood–Poole cover claim#✓fully proved

Call a nonempty set \(\Omega \subseteq \mathbb{C}\) a universal cover if every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation. This is the proposition that some universal cover has area (Lebesgue outer measure) at most \(0.260437\).

def nonconvexCoverNorwoodPoole2003 : Prop :=
  ∃ Ω : Set ℂ, IsUniversalCover Ω ∧ volume Ω ≤ ENNReal.ofReal ((2604370 : ℝ) / 10000000)
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 2
Statement usesUniversal covers
Used byNorwood–Poole universal cover for unit arcs · A Norwood–Poole cover bounds the nonconvex worm cover constant

DefinitionThe Ploymaklam–Wichiramala cover claim#✓fully proved

Call a nonempty set \(\Omega \subseteq \mathbb{C}\) a universal cover if every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation. This is the proposition that some universal cover has area (Lebesgue outer measure) at most \(0.26007\).

def nonconvexCoverPloymaklamWichiramala2018 : Prop :=
  ∃ Ω : Set ℂ, IsUniversalCover Ω ∧ volume Ω ≤ ENNReal.ofReal ((26007 : ℝ) / 100000)
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 2
Statement usesUniversal covers
Used byPloymaklam–Wichiramala universal cover for unit arcs · Covers of area at most \(0.26007\) bound the nonconvex worm cover constant

DefinitionStatement of the Norwood–Poole upper bound \(0.260437\) for worm covers#✓fully proved

The proposition that the nonconvex worm cover constant, the infimum of the areas (Lebesgue outer measures) of planar sets containing a rotated and translated copy of every planar curve of length \(1\), is at most \(0.260437\).

def nonconvexUpperBoundNorwoodPoole2003 : Prop :=
  nonconvexWormCoverConstant ≤ (2604370 : ℝ) / 10000000
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 2
Statement usesNonconvex worm cover constant
Used byA Norwood–Poole cover bounds the nonconvex worm cover constant · Norwood–Poole upper bound for the nonconvex worm cover constant

DefinitionStatement of the Ploymaklam–Wichiramala upper bound \(0.26007\) for worm covers#✓fully proved

The proposition that the nonconvex worm cover constant, the infimum of the areas (Lebesgue outer measures) of planar sets containing a rotated and translated copy of every planar curve of length \(1\), is at most \(0.26007\).

def nonconvexUpperBoundPloymaklamWichiramala2018 : Prop :=
  nonconvexWormCoverConstant ≤ (26007 : ℝ) / 100000
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 2
Statement usesNonconvex worm cover constant
Used byCovers of area at most \(0.26007\) bound the nonconvex worm cover constant · Ploymaklam–Wichiramala upper bound for the nonconvex worm cover constant

DefinitionThe positivity claim for the nonconvex worm cover constant#✓fully proved

Call a nonempty set \(\Omega \subseteq \mathbb{C}\) a universal cover if every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation, and let the nonconvex worm cover constant be the infimum of the areas (Lebesgue outer measures) of all universal covers, which is a finite real number. This is the proposition that the nonconvex worm cover constant is strictly positive.

def nonconvexStrictPositivity : Prop := 0 < nonconvexWormCoverConstant
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 1 · Used by 1
Statement usesNonconvex worm cover constant
Used byThe nonconvex worm cover constant is positive

DefinitionThe disk of diameter one covers every unit arc (claim)#✓fully proved

This proposition asserts that the closed disk \(D = \{z \in \mathbb{C} : |z| \le 1/2\}\) covers every unit arc: for every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) there are an angle \(\theta \in \mathbb{R}\) and a translation \(c \in \mathbb{C}\) such that \(e^{i\theta}\gamma(t) + c \in D\) for every \(t \in [0, 1]\).

def halfDiskCovers : Prop := CoversEveryUnitArc halfDisk
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 2 · Used by 1
Statement usesSets that cover every unit arc · Disk of radius one half
Used byThe disk of diameter one covers every unit arc

DefinitionThe half-disk of diameter one covers every unit arc (claim)#✓fully proved

This proposition asserts that the closed half-disk \(H = \{z \in \mathbb{C} : |z| \le 1/2,\ \operatorname{Im} z \ge 0\}\) covers every unit arc: for every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) there are an angle \(\theta \in \mathbb{R}\) and a translation \(c \in \mathbb{C}\) such that \(e^{i\theta}\gamma(t) + c \in H\) for every \(t \in [0, 1]\).

def halfSemidiskCovers : Prop := CoversEveryUnitArc halfSemidisk
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 2 · Used by 1
Statement usesSets that cover every unit arc · Semidisk of radius one half
Used byThe half-disk of diameter one covers every unit arc

DefinitionWetzel's sector covering claim#✓fully proved

The proposition that the closed circular sector \(S\) of radius \(1\) and angle \(30^\circ\) with apex \(0\) and symmetric about the positive real axis, that is, the set of complex numbers \(z\) with \(|z| \le 1\), \(\operatorname{Re} z \ge 0\) and \(|\operatorname{Im} z| \le \tan(\pi/12)\operatorname{Re} z\), covers every unit arc: for every continuous curve \(\gamma : [0,1] \to \mathbb{C}\) of length (total variation) exactly \(1\) there are an angle \(\theta \in \mathbb{R}\) and a point \(c \in \mathbb{C}\) such that \(e^{i\theta}\gamma(t) + c \in S\) for all \(t \in [0,1]\).

def wetzelSectorCovers : Prop := CoversEveryUnitArc wetzelSector
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 2 · Used by 1
Statement usesSets that cover every unit arc · Wetzel's sector
Used byWetzel's sector covers every unit arc

TheoremA Norwood–Poole cover bounds the nonconvex worm cover constant#✓fully proved

Call a nonempty set \(\Omega \subseteq \mathbb{C}\) a universal cover if every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation, and let the nonconvex worm cover constant be the infimum of the areas (Lebesgue outer measures) of all universal covers, which is a finite real number. If some universal cover has area at most \(0.260437\), then the nonconvex worm cover constant is at most \(0.260437\).

theorem nonconvexUpperBoundNorwoodPoole2003_of_cover
    (h : nonconvexCoverNorwoodPoole2003) : nonconvexUpperBoundNorwoodPoole2003
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 3
Statement usesThe Norwood–Poole cover claim · Statement of the Norwood–Poole upper bound \(0.260437\) for worm covers
Proof usesCovers give upper bounds on the nonconvex worm cover constant

TheoremCovers of area at most \(0.26007\) bound the nonconvex worm cover constant#✓fully proved

If some nonempty planar set of area (Lebesgue outer measure) at most \(0.26007\) contains a rotated and translated copy of every planar curve of length \(1\), then the nonconvex worm cover constant is at most \(0.26007\).

theorem nonconvexUpperBoundPloymaklamWichiramala2018_of_cover
    (h : nonconvexCoverPloymaklamWichiramala2018) :
    nonconvexUpperBoundPloymaklamWichiramala2018
Sources
  • Optimization Problems, constant 13a; source-specific interval-arc adaptation.
Uses 3
Statement usesThe Ploymaklam–Wichiramala cover claim · Statement of the Ploymaklam–Wichiramala upper bound \(0.26007\) for worm covers
Proof usesCovers give upper bounds on the nonconvex worm cover constant

TheoremThe convex worm cover constant is at most π/4#●ready to prove

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant, the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation, is at most \(\pi/4\).

theorem_wanted upperBoundPiOverFour_holds : upperBoundPiOverFour
Sources
  • Optimization Problems, constant 13a, closed claim upperBoundPiOverFour.
Uses 1
Statement usesProposition: the convex worm cover constant is at most π/4

TheoremThe convex worm cover constant is at most π/8#●ready to prove

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant, the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation, is at most \(\pi/8\).

theorem_wanted upperBoundPiOverEight_holds : upperBoundPiOverEight
Sources
  • Optimization Problems, constant 13a, closed claim upperBoundPiOverEight.
Uses 1
Statement usesProposition: the convex worm cover constant is at most π/8

TheoremThe convex worm cover constant is at most 0.34501#●ready to prove

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant, the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation, is at most \(0.34501\).

theorem_wanted upperBoundWetzel1973_holds : upperBoundWetzel1973
Sources
  • Optimization Problems, constant 13a, closed claim upperBoundWetzel1973.
Uses 1
Statement usesProposition: the convex worm cover constant is at most 0.34501

TheoremGerriets' upper bound for the convex worm cover constant#●ready to prove

Moser's convex worm cover constant, the infimum of the areas of convex planar sets containing a rotated and translated copy of every planar curve of length \(1\), is at most \(0.3214\).

theorem_wanted upperBoundGerriets1972_holds : upperBoundGerriets1972
Sources
  • Optimization Problems, constant 13a, closed claim upperBoundGerriets1972.
Uses 1
Statement usesStatement of Gerriets' upper bound \(0.3214\) for convex worm covers

TheoremGerriets–Poole upper bound for the convex worm cover constant#●ready to prove

Moser's convex worm cover constant, the infimum of the areas of convex planar sets containing a rotated and translated copy of every planar curve of length \(1\), is at most \(0.2861\).

theorem_wanted upperBoundGerrietsPoole1974_holds : upperBoundGerrietsPoole1974
Sources
  • Optimization Problems, constant 13a, closed claim upperBoundGerrietsPoole1974.
Uses 1
Statement usesStatement of the Gerriets–Poole upper bound \(0.2861\) for convex worm covers

TheoremNorwood–Poole–Laidacker upper bound for the convex worm cover constant#●ready to prove

Moser's convex worm cover constant, the infimum of the areas of convex planar sets containing a rotated and translated copy of every planar curve of length \(1\), is at most \(0.27524\).

theorem_wanted upperBoundNorwoodPooleLaidacker1992_holds : upperBoundNorwoodPooleLaidacker1992
Sources
  • Optimization Problems, constant 13a, closed claim upperBoundNorwoodPooleLaidacker1992.
Uses 1
Statement usesStatement of the Norwood–Poole–Laidacker upper bound \(0.27524\) for convex worm covers

TheoremThe convex worm cover constant is at most 0.270911861#●ready to prove

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant, the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation, is at most \(0.270911861\).

theorem_wanted upperBoundWang2006_holds : upperBoundWang2006
Sources
  • Optimization Problems, constant 13a, closed claim upperBoundWang2006.
Uses 1
Statement usesProposition: the convex worm cover constant is at most 0.270911861

TheoremThe convex worm cover constant is at most π/12#●ready to prove

A unit arc is a continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\). The convex worm cover constant, the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) that contain, for every unit arc \(\gamma\), the image of \(\gamma\) under some rotation followed by a translation, is at most \(\pi/12\).

theorem_wanted upperBoundPiOverTwelve_holds : upperBoundPiOverTwelve
Sources
  • Optimization Problems, constant 13a, closed claim upperBoundPiOverTwelve.
Uses 1
Statement usesProposition: the convex worm cover constant is at most π/12

TheoremWetzel's 1973 lower bound for the convex worm cover constant#●ready to prove

Let \(\mu\) be the convex worm cover constant, the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) such that every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by a rotation followed by a translation. Then \(0.2194 \le \mu\).

theorem_wanted lowerBoundWetzel1973_holds : lowerBoundWetzel1973
Sources
  • Optimization Problems, constant 13a, closed claim lowerBoundWetzel1973.
Uses 1
Statement usesWetzel's 1973 lower bound for the convex worm cover constant (claim)

TheoremKhandhawit–Sriswasdi 2009 lower bound for the convex worm cover constant#●ready to prove

Let \(\mu\) be the convex worm cover constant, the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) such that every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by a rotation followed by a translation. Then \(0.227498 \le \mu\).

theorem_wanted lowerBoundKhandhawitSriswasdi2009_holds : lowerBoundKhandhawitSriswasdi2009
Sources
  • Optimization Problems, constant 13a, closed claim lowerBoundKhandhawitSriswasdi2009.
Uses 1
Statement usesKhandhawit–Sriswasdi 2009 lower bound for the convex worm cover constant (claim)

TheoremKhandhawit–Pagonakis–Sriswasdi 2013 lower bound on the convex worm cover constant#●ready to prove

Let \(\mu\) be the convex worm cover constant, the infimum of the areas of the nonempty convex sets \(\Omega \subseteq \mathbb{C}\) such that every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by a rotation followed by a translation. Then \(0.232239 \le \mu\).

theorem_wanted lowerBoundKhandhawitPagonakisSriswasdi2013_holds :
    lowerBoundKhandhawitPagonakisSriswasdi2013
Sources
  • Optimization Problems, constant 13a, closed claim lowerBoundKhandhawitPagonakisSriswasdi2013.
Uses 1
Statement usesKhandhawit–Pagonakis–Sriswasdi 2013 lower bound on the convex worm cover constant (claim)

TheoremA minimal convex cover for unit arcs exists#●ready to prove

Call a nonempty convex set \(\Omega \subseteq \mathbb{C}\) a convex universal cover if every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation, and let the convex worm cover constant be the infimum of the areas (Lebesgue measures) of all convex universal covers, which is a finite real number. Then some convex universal cover has area equal to the convex worm cover constant.

theorem_wanted minimalConvexCoverExists_holds : minimalConvexCoverExists
Sources
  • Optimization Problems, constant 13a, closed claim minimalConvexCoverExists.
Uses 1
Statement usesThe minimal-convex-cover claim

TheoremNorwood–Poole universal cover for unit arcs#●ready to prove

There is a nonempty set \(\Omega \subseteq \mathbb{C}\) of area (Lebesgue outer measure) at most \(0.260437\) such that every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation.

theorem_wanted nonconvexCoverNorwoodPoole2003_holds : nonconvexCoverNorwoodPoole2003
Sources
  • Optimization Problems, constant 13a, closed claim nonconvexCoverNorwoodPoole2003.
Uses 1
Statement usesThe Norwood–Poole cover claim

TheoremPloymaklam–Wichiramala universal cover for unit arcs#●ready to prove

There is a nonempty set \(\Omega \subseteq \mathbb{C}\) of area (Lebesgue outer measure) at most \(0.26007\) such that every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation.

theorem_wanted nonconvexCoverPloymaklamWichiramala2018_holds :
    nonconvexCoverPloymaklamWichiramala2018
Sources
  • Optimization Problems, constant 13a, closed claim nonconvexCoverPloymaklamWichiramala2018.
Uses 1
Statement usesThe Ploymaklam–Wichiramala cover claim

TheoremNorwood–Poole upper bound for the nonconvex worm cover constant#●ready to prove

Call a nonempty set \(\Omega \subseteq \mathbb{C}\) a universal cover if every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation, and let the nonconvex worm cover constant be the infimum of the areas (Lebesgue outer measures) of all universal covers, which is a finite real number. Then the nonconvex worm cover constant is at most \(0.260437\).

theorem_wanted nonconvexUpperBoundNorwoodPoole2003_holds : nonconvexUpperBoundNorwoodPoole2003
Sources
  • Optimization Problems, constant 13a, closed claim nonconvexUpperBoundNorwoodPoole2003.
Uses 1
Statement usesStatement of the Norwood–Poole upper bound \(0.260437\) for worm covers

TheoremPloymaklam–Wichiramala upper bound for the nonconvex worm cover constant#●ready to prove

The nonconvex worm cover constant, the infimum of the areas (Lebesgue outer measures) of planar sets containing a rotated and translated copy of every planar curve of length \(1\), is at most \(0.26007\).

theorem_wanted nonconvexUpperBoundPloymaklamWichiramala2018_holds :
    nonconvexUpperBoundPloymaklamWichiramala2018
Sources
  • Optimization Problems, constant 13a, closed claim nonconvexUpperBoundPloymaklamWichiramala2018.
Uses 1
Statement usesStatement of the Ploymaklam–Wichiramala upper bound \(0.26007\) for worm covers

TheoremThe nonconvex worm cover constant is positive#●ready to prove

Call a nonempty set \(\Omega \subseteq \mathbb{C}\) a universal cover if every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) can be moved into \(\Omega\) by some rotation followed by a translation, and let the nonconvex worm cover constant be the infimum of the areas (Lebesgue outer measures) of all universal covers, which is a finite real number. Then the nonconvex worm cover constant is strictly positive.

theorem_wanted nonconvexStrictPositivity_holds : nonconvexStrictPositivity
Sources
  • Optimization Problems, constant 13a, closed claim nonconvexStrictPositivity.
Uses 1
Statement usesThe positivity claim for the nonconvex worm cover constant

TheoremThe disk of diameter one covers every unit arc#●ready to prove

For every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) there are an angle \(\theta \in \mathbb{R}\) and a translation \(c \in \mathbb{C}\) such that \(|e^{i\theta}\gamma(t) + c| \le 1/2\) for every \(t \in [0, 1]\).

theorem_wanted halfDiskCovers_holds : halfDiskCovers
Sources
  • Optimization Problems, constant 13a, closed claim halfDiskCovers.
Uses 1
Statement usesThe disk of diameter one covers every unit arc (claim)

TheoremThe half-disk of diameter one covers every unit arc#●ready to prove

Let \(H = \{z \in \mathbb{C} : |z| \le 1/2,\ \operatorname{Im} z \ge 0\}\). For every continuous curve \(\gamma : [0, 1] \to \mathbb{C}\) of length exactly \(1\) there are an angle \(\theta \in \mathbb{R}\) and a translation \(c \in \mathbb{C}\) such that \(e^{i\theta}\gamma(t) + c \in H\) for every \(t \in [0, 1]\).

theorem_wanted halfSemidiskCovers_holds : halfSemidiskCovers
Sources
  • Optimization Problems, constant 13a, closed claim halfSemidiskCovers.
Uses 1
Statement usesThe half-disk of diameter one covers every unit arc (claim)

TheoremWetzel's sector covers every unit arc#●ready to prove

Let \(S\) be the closed circular sector of radius \(1\) and angle \(30^\circ\) with apex \(0\) and symmetric about the positive real axis, that is, the set of complex numbers \(z\) with \(|z| \le 1\), \(\operatorname{Re} z \ge 0\) and \(|\operatorname{Im} z| \le \tan(\pi/12)\operatorname{Re} z\). Then for every continuous curve \(\gamma : [0,1] \to \mathbb{C}\) of length (total variation) exactly \(1\) there are an angle \(\theta \in \mathbb{R}\) and a point \(c \in \mathbb{C}\) such that \(e^{i\theta}\gamma(t) + c \in S\) for all \(t \in [0,1]\).

theorem_wanted wetzelSectorCovers_holds : wetzelSectorCovers
Sources
  • Optimization Problems, constant 13a, closed claim wetzelSectorCovers.
Uses 1
Statement usesWetzel's sector covering claim
56 fully proved20 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.