Lebesgue's universal covering problem

AbbreviationThe Euclidean plane of Lebesgue's covering problem#✓fully proved

The ambient space is the Euclidean plane \(\mathbb{R}^2\), with the Euclidean distance.

abbrev Plane := EuclideanSpace ℝ (Fin 2)

Used by 9

Used byAreas of universal convex covers · Covering a congruent copy · Directional width · Statement of the existence of a minimal universal convex cover · Sets of constant width one · Convex sets of diameter one · Universal convex covers · Planar area · Covering sets of constant width one suffices (statement)

DefinitionConvex sets of diameter one#✓fully proved

A set \(K\) in the Euclidean plane \(\mathbb{R}^2\) is a unit-diameter convex set when it is nonempty and convex and its diameter \(\sup_{x, y \in K} \lVert x - y \rVert\) is exactly \(1\).

def IsUnitDiameterConvexSet (K : Set Plane) : Prop :=
  K.Nonempty ∧ Convex ℝ K ∧ Metric.diam K = 1

Uses 1 · Used by 1

Statement usesThe Euclidean plane of Lebesgue's covering problem

Used byUniversal convex covers

DefinitionCovering a congruent copy#✓fully proved

A planar set \(\Omega\) covers a congruent copy of a planar set \(K\) when some isometry \(e\) of the plane onto itself satisfies \(e(K) \subseteq \Omega\).

Isometries include reflections.

def CoversCongruentCopy (Ω K : Set Plane) : Prop :=
  ∃ e : Plane ≃ᵢ Plane, e '' K ⊆ Ω

Uses 1 · Used by 2

Statement usesThe Euclidean plane of Lebesgue's covering problem

Used byUniversal convex covers · Covering sets of constant width one suffices (statement)

DefinitionUniversal convex covers#✓fully proved

A set \(\Omega\) in the Euclidean plane \(\mathbb{R}^2\) is a universal convex cover when it is nonempty and convex and, for every nonempty convex set \(K \subseteq \mathbb{R}^2\) of diameter \(1\), some isometry \(e\) of the plane onto itself satisfies \(e(K) \subseteq \Omega\).

def IsUniversalConvexCover (Ω : Set Plane) : Prop :=
  Ω.Nonempty ∧ Convex ℝ Ω ∧
    ∀ K : Set Plane, IsUnitDiameterConvexSet K → CoversCongruentCopy Ω K

Uses 3 · Used by 3

Statement usesCovering a congruent copy · Convex sets of diameter one · The Euclidean plane of Lebesgue's covering problem

Used byAreas of universal convex covers · Statement of the existence of a minimal universal convex cover · Covering sets of constant width one suffices (statement)

DefinitionPlanar area#✓fully proved

The area of a set \(S\) in the Euclidean plane \(\mathbb{R}^2\) is its Lebesgue measure (outer measure if \(S\) is not measurable), a value in \([0, \infty]\), so infinite area is allowed.

def planarArea (S : Set Plane) : ENNReal :=
  volume S

Uses 1 · Used by 2

Statement usesThe Euclidean plane of Lebesgue's covering problem

Used byAreas of universal convex covers · Statement of the existence of a minimal universal convex cover

DefinitionAreas of universal convex covers#✓fully proved

The set of admissible cover areas is the set of all \(a \in [0, \infty]\) for which there is a universal convex cover \(\Omega\) in the plane (a nonempty convex set containing a congruent copy of every nonempty convex planar set of diameter \(1\)) whose Lebesgue area is \(a\).

def admissibleCoverAreas : Set ENNReal :=
  {a | ∃ Ω : Set Plane, IsUniversalConvexCover Ω ∧ planarArea Ω = a}

Uses 3 · Used by 1

Statement usesUniversal convex covers · The Euclidean plane of Lebesgue's covering problem · Planar area

Used byLebesgue universal covering constant

DefinitionLebesgue universal covering constant#✓fully proved

Call a set \(\Omega\) in the Euclidean plane \(\mathbb{R}^2\) a universal convex cover if it is nonempty and convex and, for every nonempty convex set \(K \subseteq \mathbb{R}^2\) of diameter exactly \(1\), some isometry of the plane onto itself maps \(K\) into \(\Omega\). The Lebesgue universal covering constant is the infimum, taken in \([0, \infty]\), of the Lebesgue areas of all universal convex covers; the infimum of an empty family would be \(\infty\).

The definition does not assume that a universal convex cover of minimal area exists.

def lebesgueUniversalCoveringConstant : ENNReal :=
  sInf admissibleCoverAreas

Uses 1 · Used by 12

Statement usesAreas of universal convex covers

Used byStatement of the Baez–Bagdasaryan–Gibbs upper bound · Statement of the Brass–Sharifi lower bound · Statement of Elekes's disk-and-triangle lower bound · Statement of the existence of a minimal universal convex cover · Statement of Elekes's regular-polygon lower bound · Statement of Gibbs's upper bound · Statement of Hansen's corrected upper bound · Statement of Pál's hexagon bound · Statement of Pál's truncated hexagon bound · Statement of Sprague's bound · Jung's upper bound for Lebesgue's universal covering constant (statement) · Disk lower bound for Lebesgue's universal covering constant (statement)

DefinitionDirectional width#✓fully proved

For a planar set \(K\) and a vector \(u\) in the plane, the width of \(K\) in direction \(u\) is \(\sup_{x \in K} \langle u, x \rangle - \inf_{x \in K} \langle u, x \rangle\), where the supremum and infimum are taken in \(\mathbb{R}\), with the convention that each is \(0\) when the set of values \(\langle u, x \rangle\) is empty or unbounded on that side.

It is only applied to nonempty compact \(K\), where both extrema are attained.

def directionalWidth (K : Set Plane) (u : Plane) : ℝ :=
  sSup ((fun x : Plane => inner ℝ u x) '' K) -
    sInf ((fun x : Plane => inner ℝ u x) '' K)

Uses 1 · Used by 1

Statement usesThe Euclidean plane of Lebesgue's covering problem

Used bySets of constant width one

DefinitionSets of constant width one#✓fully proved

A set \(K\) in the Euclidean plane \(\mathbb{R}^2\) has constant width \(1\) when it is nonempty, compact and convex and, for every unit vector \(u\), its width in direction \(u\), namely \(\sup_{x \in K} \langle u, x \rangle - \inf_{x \in K} \langle u, x \rangle\), equals \(1\).

def IsConstantWidthOne (K : Set Plane) : Prop :=
  K.Nonempty ∧ IsCompact K ∧ Convex ℝ K ∧
    ∀ u : Plane, ‖u‖ = 1 → directionalWidth K u = 1

Uses 2 · Used by 1

Statement usesThe Euclidean plane of Lebesgue's covering problem · Directional width

Used byCovering sets of constant width one suffices (statement)

DefinitionStatement of the existence of a minimal universal convex cover#✓fully proved

This proposition states that some nonempty convex set \(\Omega\) in the Euclidean plane \(\mathbb{R}^2\) is a universal convex cover, that is, for every nonempty convex set \(K \subseteq \mathbb{R}^2\) of diameter \(1\) some isometry \(e\) of the plane onto itself satisfies \(e(K) \subseteq \Omega\), and that the area (planar Lebesgue measure) of \(\Omega\) equals the Lebesgue universal covering constant, the infimum of the areas of all universal convex covers.

The existence of such a cover follows from the Blaschke selection theorem.

def elekes1994MinimalCoverExists : Prop :=
  ∃ Ω : Set Plane,
    IsUniversalConvexCover Ω ∧
      planarArea Ω = lebesgueUniversalCoveringConstant

Uses 4 · Used by 1

Statement usesUniversal convex covers · The Euclidean plane of Lebesgue's covering problem · Lebesgue universal covering constant · Planar area

Used byExistence of a minimal universal cover

DefinitionCovering sets of constant width one suffices (statement)#✓fully proved

The proposition that every nonempty convex subset \(\Omega\) of the Euclidean plane that contains a congruent copy of every nonempty compact convex planar set of constant width \(1\) is a universal convex cover, that is, contains a congruent copy of every nonempty convex planar set of diameter \(1\).

def vrecica1981ConstantWidthOneSuffices : Prop :=
  ∀ Ω : Set Plane,
    Ω.Nonempty →
      Convex ℝ Ω →
        (∀ K : Set Plane, IsConstantWidthOne K → CoversCongruentCopy Ω K) →
          IsUniversalConvexCover Ω

Uses 4 · Used by 1

Statement usesCovering a congruent copy · Sets of constant width one · Universal convex covers · The Euclidean plane of Lebesgue's covering problem

Used byCovering sets of constant width one suffices

DefinitionJung's upper bound for Lebesgue's universal covering constant (statement)#✓fully proved

The proposition that Lebesgue's universal covering constant is at most \(\pi/3\).

This is the bound given by Jung's theorem: a closed disk of radius \(1/\sqrt{3}\), of area \(\pi/3\), contains a translate of every planar set of diameter \(1\).

def trivialJungElekes1994UpperBound : Prop :=
  lebesgueUniversalCoveringConstant ≤ ENNReal.ofReal (Real.pi / 3)

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byJung's bound for the Lebesgue covering problem

DefinitionStatement of Pál's hexagon bound#✓fully proved

The proposition that the Lebesgue universal covering constant is at most \(\sqrt{3}/2\), the bound given by Pál's regular hexagon.

def pal1920HexagonUpperBound : Prop :=
  lebesgueUniversalCoveringConstant ≤ ENNReal.ofReal (Real.sqrt 3 / 2)

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byPál's hexagon bound

DefinitionStatement of Pál's truncated hexagon bound#✓fully proved

The proposition that the Lebesgue universal covering constant is at most \(2 - 2/\sqrt{3}\), the bound given by Pál's truncated hexagon.

def pal1920TruncatedHexagonUpperBound : Prop :=
  lebesgueUniversalCoveringConstant ≤
    ENNReal.ofReal (2 - 2 / Real.sqrt 3)

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byPál's truncated hexagon bound

DefinitionStatement of Sprague's bound#✓fully proved

The proposition that the Lebesgue universal covering constant is at most \(0.844137708436\).

def sprague1936UpperBound : Prop :=
  lebesgueUniversalCoveringConstant ≤ ENNReal.ofReal 0.844137708436

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used bySprague's bound

DefinitionStatement of Hansen's corrected upper bound#✓fully proved

This proposition states that the Lebesgue universal covering constant, the infimum of the areas of the nonempty convex sets in the Euclidean plane that contain a congruent copy of every nonempty convex planar set of diameter \(1\), is at most \(0.844137708398\).

This is Hansen's finite-decimal upper bound, as corrected by Baez, Bagdasaryan and Gibbs.

def hansen1992CorrectedBBG2015UpperBound : Prop :=
  lebesgueUniversalCoveringConstant ≤ ENNReal.ofReal 0.844137708398

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byHansen's upper bound for Lebesgue's covering problem, as corrected

DefinitionStatement of the Baez–Bagdasaryan–Gibbs upper bound#✓fully proved

This is the proposition that there is a real number \(b\) with \(0.844115297128419059 \le b < 0.844115297128419060\) such that the Lebesgue universal covering constant (the infimum of the areas of universal convex covers) is at most \(b\).

The 18 printed digits are a truncation of the bound, not its exact value.

def bbg2015ApproximateUpperBound : Prop :=
  ∃ b : ℝ,
    0.844115297128419059 ≤ b ∧
      b < 0.844115297128419060 ∧
        lebesgueUniversalCoveringConstant ≤ ENNReal.ofReal b

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byBaez–Bagdasaryan–Gibbs upper bound

DefinitionStatement of Gibbs's upper bound#✓fully proved

This proposition states that the Lebesgue universal covering constant, the infimum of the areas of the nonempty convex sets in the Euclidean plane that contain a congruent copy of every nonempty convex planar set of diameter \(1\), is at most \(0.8440935944\).

def gibbs2018UpperBound : Prop :=
  lebesgueUniversalCoveringConstant ≤ ENNReal.ofReal 0.8440935944

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byGibbs's upper bound for Lebesgue's covering problem

DefinitionDisk lower bound for Lebesgue's universal covering constant (statement)#✓fully proved

The proposition that Lebesgue's universal covering constant is at least \(\pi/4\).

This is the bound given by a disk of radius \(1/2\), which has diameter \(1\) and area \(\pi/4\).

def trivialUnitDiskLowerBound : Prop :=
  ENNReal.ofReal (Real.pi / 4) ≤ lebesgueUniversalCoveringConstant

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byDisk lower bound for Lebesgue's universal covering constant

DefinitionStatement of Elekes's disk-and-triangle lower bound#✓fully proved

This is the proposition that the Lebesgue universal covering constant (the infimum of the areas of universal convex covers) is at least \(0.8257\).

The bound comes from simultaneously covering a disk and an equilateral triangle of diameter \(1\).

def elekes1994DiskTriangleLowerBound : Prop :=
  ENNReal.ofReal 0.8257 ≤ lebesgueUniversalCoveringConstant

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byElekes's disk-and-triangle lower bound

DefinitionStatement of Elekes's regular-polygon lower bound#✓fully proved

This proposition states that the Lebesgue universal covering constant, the infimum of the areas of the nonempty convex sets in the Euclidean plane that contain a congruent copy of every nonempty convex planar set of diameter \(1\), is at least \(0.8271\).

This is Elekes's finite-decimal lower bound, obtained using regular \(3^j\)-gons as well.

def elekes1994RegularPolygonLowerBound : Prop :=
  ENNReal.ofReal 0.8271 ≤ lebesgueUniversalCoveringConstant

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byElekes's regular-polygon lower bound for Lebesgue's covering problem

DefinitionStatement of the Brass–Sharifi lower bound#✓fully proved

This is the proposition that the Lebesgue universal covering constant (the infimum of the areas of universal convex covers) is at least \(0.832\).

Brass and Sharifi obtained this bound by a rigorous computer-aided argument.

def brassSharifi2005LowerBound : Prop :=
  ENNReal.ofReal 0.832 ≤ lebesgueUniversalCoveringConstant

Uses 1 · Used by 1

Statement usesLebesgue universal covering constant

Used byBrass–Sharifi lower bound

TheoremExistence of a minimal universal cover#●ready to prove

There is a universal convex cover \(\Omega\) (a nonempty convex planar set containing a congruent copy of every nonempty convex planar set of diameter \(1\)) whose Lebesgue area equals the Lebesgue universal covering constant, the infimum of the areas of all universal convex covers.

theorem_wanted elekes1994MinimalCoverExists_holds : elekes1994MinimalCoverExists

Sources

• Elekes, Generalized breadths, circular Cantor sets, and the least area UCC (1994).

Uses 1

Statement usesStatement of the existence of a minimal universal convex cover

TheoremCovering sets of constant width one suffices#●ready to prove

Let \(\Omega\) be a nonempty convex subset of the Euclidean plane that contains a congruent copy (an image under an isometry of the plane, reflections allowed) of every nonempty compact convex planar set of constant width \(1\). Then \(\Omega\) contains a congruent copy of every nonempty convex planar set of diameter \(1\), that is, \(\Omega\) is a universal convex cover.

theorem_wanted vrecica1981ConstantWidthOneSuffices_holds : vrecica1981ConstantWidthOneSuffices

Sources

• Vrećica, A note on sets of constant width (1981).

Uses 1

Statement usesCovering sets of constant width one suffices (statement)

TheoremJung's bound for the Lebesgue covering problem#●ready to prove

The Lebesgue universal covering constant is at most \(\pi/3\).

theorem_wanted trivialJungElekes1994UpperBound_holds : trivialJungElekes1994UpperBound

Sources

• Jung's theorem, quoted in Elekes (1994), catalogue constant 13b.

Uses 1

Statement usesJung's upper bound for Lebesgue's universal covering constant (statement)

TheoremPál's hexagon bound#●ready to prove

The Lebesgue universal covering constant is at most \(\sqrt{3}/2\).

theorem_wanted pal1920HexagonUpperBound_holds : pal1920HexagonUpperBound

Sources

• Pál, Über ein elementares Variationsproblem (1920), hexagon bound.

Uses 1

Statement usesStatement of Pál's hexagon bound

TheoremPál's truncated hexagon bound#●ready to prove

The Lebesgue universal covering constant is at most \(2 - 2/\sqrt{3}\).

theorem_wanted pal1920TruncatedHexagonUpperBound_holds : pal1920TruncatedHexagonUpperBound

Sources

• Pál, Über ein elementares Variationsproblem (1920), truncated hexagon bound.

Uses 1

Statement usesStatement of Pál's truncated hexagon bound

TheoremSprague's bound#●ready to prove

The Lebesgue universal covering constant is at most \(0.844137708436\).

theorem_wanted sprague1936UpperBound_holds : sprague1936UpperBound

Sources

• Sprague, Über ein elementares Variationsproblem (1936).

Uses 1

Statement usesStatement of Sprague's bound

TheoremHansen's upper bound for Lebesgue's covering problem, as corrected#●ready to prove

The Lebesgue universal covering constant, the infimum of the areas of the nonempty convex sets in the Euclidean plane that contain a congruent copy of every nonempty convex planar set of diameter \(1\), is at most \(0.844137708398\).

theorem_wanted hansen1992CorrectedBBG2015UpperBound_holds : hansen1992CorrectedBBG2015UpperBound

Sources

• Hansen (1992), corrected in Baez, Bagdasaryan and Gibbs (2015).

Uses 1

Statement usesStatement of Hansen's corrected upper bound

TheoremBaez–Bagdasaryan–Gibbs upper bound#●ready to prove

There is a real number \(b\) with \(0.844115297128419059 \le b < 0.844115297128419060\) such that the Lebesgue universal covering constant (the infimum of the areas of universal convex covers) is at most \(b\).

theorem_wanted bbg2015ApproximateUpperBound_holds : bbg2015ApproximateUpperBound

Sources

• Baez, Bagdasaryan and Gibbs, The Lebesgue universal covering problem (2015).

Uses 1

Statement usesStatement of the Baez–Bagdasaryan–Gibbs upper bound

TheoremGibbs's upper bound for Lebesgue's covering problem#●ready to prove

The Lebesgue universal covering constant, the infimum of the areas of the nonempty convex sets in the Euclidean plane that contain a congruent copy of every nonempty convex planar set of diameter \(1\), is at most \(0.8440935944\).

theorem_wanted gibbs2018UpperBound_holds : gibbs2018UpperBound

Sources

• Gibbs, An Upper Bound for Lebesgue's Covering Problem (2018).

Uses 1

Statement usesStatement of Gibbs's upper bound

TheoremDisk lower bound for Lebesgue's universal covering constant#●ready to prove

Lebesgue's universal covering constant, the infimum of the areas of the nonempty convex planar sets that contain a congruent copy of every nonempty convex planar set of diameter \(1\), is at least \(\pi/4\), the area of a disk of radius \(1/2\).

theorem_wanted trivialUnitDiskLowerBound_holds : trivialUnitDiskLowerBound

Sources

• Radius-half disk lower-bound row, optimization catalogue constant 13b.

Uses 1

Statement usesDisk lower bound for Lebesgue's universal covering constant (statement)

TheoremElekes's disk-and-triangle lower bound#●ready to prove

The Lebesgue universal covering constant (the infimum of the areas of universal convex covers) is at least \(0.8257\).

theorem_wanted elekes1994DiskTriangleLowerBound_holds : elekes1994DiskTriangleLowerBound

Sources

• Elekes (1994), disk and equilateral triangle lower bound.

Uses 1

Statement usesStatement of Elekes's disk-and-triangle lower bound

TheoremElekes's regular-polygon lower bound for Lebesgue's covering problem#●ready to prove

The Lebesgue universal covering constant, the infimum of the areas of the nonempty convex sets in the Euclidean plane that contain a congruent copy of every nonempty convex planar set of diameter \(1\), is at least \(0.8271\).

theorem_wanted elekes1994RegularPolygonLowerBound_holds : elekes1994RegularPolygonLowerBound

Sources

• Elekes (1994), additional regular polygon lower bound.

Uses 1

Statement usesStatement of Elekes's regular-polygon lower bound

TheoremBrass–Sharifi lower bound#●ready to prove

The Lebesgue universal covering constant (the infimum of the areas of universal convex covers) is at least \(0.832\).

theorem_wanted brassSharifi2005LowerBound_holds : brassSharifi2005LowerBound

Sources

• Brass and Sharifi, A lower bound for Lebesgue's universal cover problem (2005).

Uses 1

Statement usesStatement of the Brass–Sharifi lower bound

22 fully proved13 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.