Moser's Worm

Reference: Wikipedia

def Worms : Set (Set (EuclideanSpace ℝ (Fin 2)))

The set of worms is the set of curves of length (at most) 1. We formalize this as the set of ranges of 1-Lipschitz functions from [0,1] to ℝ².

Equations

• Worms = {s : Set (EuclideanSpace ℝ (Fin 2)) | ∃ (f : ↑(Set.Icc 0 1) → EuclideanSpace ℝ (Fin 2)), LipschitzWith 1 f ∧ Set.range f = s}

def WormCovers : Set (Set (EuclideanSpace ℝ (Fin 2)))

The set of covers is the set of (measurable) sets that cover every worm by translation and rotation (i.e. through an isometry).

Equations

• WormCovers = {X : Set (EuclideanSpace ℝ (Fin 2)) | MeasurableSet X ∧ ∀ w ∈ Worms, ∃ (iso : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)), Isometry iso ∧ w ⊆ iso '' X}

theorem disc_mem_worm_covers : Metric.closedBall 0 0.5 ∈ WormCovers

A disc of radius 1 / 2 is a worm cover.

This follows by translating the center of the disc to the midpoint of the worm.

theorem mosers_worm_problem : IsGLB {v : ENNReal | ∃ X ∈ WormCovers, MeasureTheory.volume X = v} sorry

Moser's Worm Problem What is the minimal area (or greatest lower bound on the area) of a shape that can cover every unit-length curve?

theorem mosers_worm_problem_upper_bound : ∃ X ∈ WormCovers, MeasureTheory.volume X = 0.260437

There is a set of area 0.260437 that covers all worms.

Reference: Norwood, Rick; Poole, George (2003), "An improved upper bound for Leo Moser's worm problem", Discrete and Computational Geometry, 29 (3): 409–417, doi:10.1007/s00454-002-0774-3, MR 1961007.

theorem convex_mosers_worm_problem : IsGLB {v : ENNReal | ∃ X ∈ WormCovers, Convex ℝ X ∧ MeasureTheory.volume X = v} sorry

Convex Moser's Worm Problem What is the minimal area (or greatest lower bound on the area) of a convex shape that can cover every unit-length curve?

theorem convex_mosers_worm_problem_bound_attained : ∃ (bound : ENNReal), IsLeast {v : ENNReal | ∃ X ∈ WormCovers, Convex ℝ X ∧ MeasureTheory.volume X = v} bound

The minimal area of a convex shape that can cover every unit-length curve is attained. This follows from the Blaschke selection theorem.

theorem convex_mosers_worm_problem_upper_bound : ∃ (X : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet X ∧ Convex ℝ X ∧ MeasureTheory.volume X = 0.270911861 ∧ ∀ w ∈ Worms, ∃ (iso : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)), Isometry iso ∧ w ⊆ iso '' X

There is a convex set of area 0.270911861 that covers all worms.

Reference: Wang, Wei (2006), "An improved upper bound for the worm problem", Acta Mathematica Sinica, 49 (4): 835–846, MR 2264090.

theorem convex_mosers_worm_problem_lower_bound : 0.232239 ∈ lowerBounds {v : ENNReal | ∃ X ∈ WormCovers, Convex ℝ X ∧ MeasureTheory.volume X = v}

0.232239 is a lower bound on the area of a convex set that covers all worms.

Reference: Khandhawit, Tirasan; Pagonakis, Dimitrios; Sriswasdi, Sira (2013), "Lower Bound for Convex Hull Area and Universal Cover Problems", International Journal of Computational Geometry & Applications, 23 (3): 197–212, arXiv:1101.5638, doi:10.1142/S0218195913500076, MR 3158583, S2CID 207132316.