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.
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem convex_mosers_worm_problem_upper_bound :
∃ X : Set ℝ², MeasurableSet X ∧ Convex ℝ X ∧ volume X = 0.270911861 ∧
∀ w ∈ Worms, ∃ (e : ℝ² ≃ₗᵢ[ℝ] ℝ²) (v : ℝ²), e.toLinearEquiv.det = 1 ∧ w ⊆ (fun x => e x + v) '' X
