Hadwiger covering and illumination problem

DefinitionConvex bodies in Euclidean space#✓fully proved

A set \(K\) in the Euclidean space \(\mathbb{R}^n\) is a convex body when it is compact and convex and its interior in \(\mathbb{R}^n\) is nonempty.

def IsConvexBody {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) : Prop :=
  IsCompact K ∧ Convex ℝ K ∧ (interior K).Nonempty

Used by 12

Used byThe coordinate cube is a convex body · Directional and exterior-point illumination are equivalent · Directional and exterior-point illumination numbers are equal · Directional illumination is equivalent to covering by smaller homothets · Directional illumination number equals the interior-translate covering number · Directional illumination is equivalent to covering by interior translates · Two equivalent formulations of Hadwiger's covering conjecture · Every convex body has a finite illumination number · Uniform covering by interior translates and uniform directional illumination · Uniform bound for covering convex bodies by interior translates · Uniform covering of symmetric bodies and uniform illumination by external points · Uniform bound for covering centrally symmetric convex bodies by interior translates

DefinitionCovering by translates#✓fully proved

For sets \(K\) and \(L\) in the Euclidean space \(\mathbb{R}^n\) and a natural number \(q\), \(K\) is covered by \(q\) translates of \(L\) when there are vectors \(v_1, \dots, v_q \in \mathbb{R}^n\) with \(K \subseteq \bigcup_{i=1}^{q} (v_i + L)\), where \(v + L = \{v + y : y \in L\}\).

def CoveredByTranslates {n : ℕ} (K L : Set (EuclideanSpace ℝ (Fin n))) (q : ℕ) : Prop :=
  ∃ translations : Fin q → EuclideanSpace ℝ (Fin n),
    K ⊆ ⋃ i, (fun x ↦ translations i + x) '' L

Used by 5

Used byCovering by interior translates · Interior-translate covers unfold to translate covers · Pointwise form of covering by translates · Translate covering number · The translate covering number is the least covering count

DefinitionCovering by interior translates#✓fully proved

A set \(K\) in the Euclidean space \(\mathbb{R}^n\) is covered by \(q\) interior translates, for a natural number \(q\), when there are vectors \(v_1, \dots, v_q \in \mathbb{R}^n\) such that \(K \subseteq \bigcup_{i=1}^{q} (v_i + \operatorname{int} K)\), where \(\operatorname{int} K\) is the interior of \(K\) in \(\mathbb{R}^n\) and \(v + S = \{v + y : y \in S\}\).

def CoveredByInteriorTranslates {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n)))
    (q : ℕ) : Prop :=
  CoveredByTranslates K (interior K) q

Uses 1 · Used by 7

Statement usesCovering by translates

Used byCovering the cube by translates of its interior needs \(2^n\) translates · Eight translates of the interior cover the three-dimensional cube · Eight is the least number of interior translates covering the three-dimensional cube · Interior-translate covers unfold to translate covers · Directional illumination is equivalent to covering by interior translates · Uniform bound for covering convex bodies by interior translates · Uniform bound for covering centrally symmetric convex bodies by interior translates

DefinitionUniform bound for covering convex bodies by interior translates#✓fully proved

For \(n, q \in \mathbb{N}\), the uniform interior translate bound holds when every convex body \(K \subseteq \mathbb{R}^n\) (a compact convex set with nonempty interior) is covered by \(q\) translates of its interior \(\operatorname{int} K\), that is, \(K \subseteq (v_1 + \operatorname{int} K) \cup \dots \cup (v_q + \operatorname{int} K)\) for some \(v_1, \dots, v_q \in \mathbb{R}^n\).

This is one bound \(q\) for all bodies at once, not a minimum over bodies.

def UniformInteriorTranslateBound (n q : ℕ) : Prop :=
  ∀ K : Set (EuclideanSpace ℝ (Fin n)),
    IsConvexBody K → CoveredByInteriorTranslates K q

Uses 2 · Used by 8

Statement usesCovering by interior translates · Convex bodies in Euclidean space

Used byUniform interior-translate bounds in dimension three are at least eight · Hadwiger covering number · A least uniform bound is the Hadwiger covering number · Two equivalent formulations of Hadwiger's covering conjecture · Papadoperakis's bound for Hadwiger's covering problem in dimension 3 · Prymak's bound for Hadwiger's covering problem in dimension 3 · Uniform covering by interior translates and uniform directional illumination · Lower bound \(2^n\) for uniform interior-translate covering

DefinitionCentral symmetry about some center#✓fully proved

A set \(K\) in the Euclidean space \(\mathbb{R}^n\) is centrally symmetric when there is a point \(c \in \mathbb{R}^n\) such that for every \(x \in \mathbb{R}^n\), \(x \in K\) if and only if \(2c - x \in K\).

def IsCentrallySymmetric {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) : Prop :=
  ∃ c : EuclideanSpace ℝ (Fin n),
    ∀ x, x ∈ K ↔ c + c - x ∈ K

Used by 3

Used byThe coordinate cube is centrally symmetric · Uniform covering of symmetric bodies and uniform illumination by external points · Uniform bound for covering centrally symmetric convex bodies by interior translates

DefinitionUniform bound for covering centrally symmetric convex bodies by interior translates#✓fully proved

For \(n, q \in \mathbb{N}\), the uniform symmetric interior translate bound holds when every convex body \(K \subseteq \mathbb{R}^n\) (a compact convex set with nonempty interior) that is centrally symmetric, meaning that there is \(c \in \mathbb{R}^n\) such that for all \(x \in \mathbb{R}^n\), \(x \in K\) if and only if \(2c - x \in K\), is covered by \(q\) translates of its interior, that is, \(K \subseteq (v_1 + \operatorname{int} K) \cup \dots \cup (v_q + \operatorname{int} K)\) for some \(v_1, \dots, v_q \in \mathbb{R}^n\).

def UniformSymmetricInteriorTranslateBound (n q : ℕ) : Prop :=
  ∀ K : Set (EuclideanSpace ℝ (Fin n)),
    IsConvexBody K → IsCentrallySymmetric K → CoveredByInteriorTranslates K q

Uses 3 · Used by 5

Statement usesCovering by interior translates · Central symmetry about some center · Convex bodies in Euclidean space

Used byLassak's theorem for centrally symmetric bodies in dimension 3 · Symmetric Hadwiger covering number · A least uniform bound is the symmetric Hadwiger covering number · Lower bound \(2^n\) for centrally symmetric interior-translate covering · Uniform covering of symmetric bodies and uniform illumination by external points

DefinitionCovering by smaller positive homothets#✓fully proved

A set \(K\) in the Euclidean space \(\mathbb{R}^n\) is covered by \(q\) smaller positive homothets, for a natural number \(q\), when there are real numbers \(r_1, \dots, r_q\) with \(0 < r_i < 1\) for every \(i\) and vectors \(v_1, \dots, v_q \in \mathbb{R}^n\) such that every point of \(K\) lies in \(v_i + r_i K = \{v_i + r_i y : y \in K\}\) for some \(i\).

The homothets are indexed by \(i\), so the same homothet may occur more than once.

def CoveredBySmallerPositiveHomothets {n : ℕ}
    (K : Set (EuclideanSpace ℝ (Fin n))) (q : ℕ) : Prop :=
  ∃ (r : Fin q → ℝ) (v : Fin q → EuclideanSpace ℝ (Fin n)),
    (∀ i, 0 < r i ∧ r i < 1) ∧
      ∀ x ∈ K, ∃ i, x ∈ (fun y ↦ v i + r i • y) '' K

Used by 2

Used byDirectional illumination is equivalent to covering by smaller homothets · Two equivalent formulations of Hadwiger's covering conjecture

DefinitionTranslate covering number#✓fully proved

For sets \(K, L \subseteq \mathbb{R}^n\), the translate covering number of \(K\) by \(L\) is the least natural number \(q\) for which there are vectors \(v_1, \dots, v_q \in \mathbb{R}^n\) with \(K \subseteq (v_1 + L) \cup \dots \cup (v_q + L)\), and it is \(\infty\) if no such \(q\) exists.

noncomputable def translateCoveringNumber {n : ℕ}
    (K L : Set (EuclideanSpace ℝ (Fin n))) : WithTop ℕ :=
  sInf ((fun q : ℕ ↦ (q : WithTop ℕ)) '' {q : ℕ | CoveredByTranslates K L q})

Uses 1 · Used by 3

Statement usesCovering by translates

Used byTranslate covering number of the three-dimensional cube by its interior · Directional illumination number equals the interior-translate covering number · The translate covering number is the least covering count

DefinitionHadwiger covering number#✓fully proved

The Hadwiger covering number of dimension \(n\), an element of \(\mathbb{N} \cup \{\infty\}\), is the least natural number \(q\) such that every convex body \(K\) in the Euclidean space \(\mathbb{R}^n\) is covered by \(q\) translates of its interior \(\operatorname{int} K\), and it is \(\infty\) if no such \(q\) exists.

noncomputable def hadwigerCoveringNumber (n : ℕ) : WithTop ℕ :=
  sInf ((fun q : ℕ ↦ (q : WithTop ℕ)) '' {q : ℕ | UniformInteriorTranslateBound n q})

Uses 1 · Used by 1

Statement usesUniform bound for covering convex bodies by interior translates

Used byA least uniform bound is the Hadwiger covering number

DefinitionSymmetric Hadwiger covering number#✓fully proved

For \(n \in \mathbb{N}\), the symmetric Hadwiger covering number in dimension \(n\) is the least natural number \(q\) such that every centrally symmetric convex body \(K \subseteq \mathbb{R}^n\) (a compact convex set with nonempty interior that is symmetric about some point) is covered by \(q\) translates of its interior, and it is \(\infty\) if no such \(q\) exists.

noncomputable def symmetricHadwigerCoveringNumber (n : ℕ) : WithTop ℕ :=
  sInf ((fun q : ℕ ↦ (q : WithTop ℕ)) ''
    {q : ℕ | UniformSymmetricInteriorTranslateBound n q})

Uses 1 · Used by 1

Statement usesUniform bound for covering centrally symmetric convex bodies by interior translates

Used byA least uniform bound is the symmetric Hadwiger covering number

TheoremPointwise form of covering by translates#✓fully proved

For sets \(K\) and \(L\) in the Euclidean space \(\mathbb{R}^n\) and a natural number \(q\), \(K\) is covered by \(q\) translates of \(L\) if and only if there are vectors \(v_1, \dots, v_q \in \mathbb{R}^n\) such that every \(x \in K\) lies in \(v_i + L = \{v_i + y : y \in L\}\) for some \(i\).

theorem coveredByTranslates_iff {n q : ℕ}
    (K L : Set (EuclideanSpace ℝ (Fin n))) :
    CoveredByTranslates K L q ↔
      ∃ v : Fin q → EuclideanSpace ℝ (Fin n), ∀ x ∈ K, ∃ i, x ∈ (fun y ↦ v i + y) '' L

Uses 1

Statement usesCovering by translates

TheoremInterior-translate covers unfold to translate covers#✓fully proved

For every set \(K\) in the Euclidean space \(\mathbb{R}^n\) and every natural number \(q\), \(K\) has a cover by \(q\) interior translates if and only if \(K\) is covered by \(q\) translates of the set \(L = \operatorname{int} K\), the interior of \(K\) in \(\mathbb{R}^n\).

theorem coveredByInteriorTranslates_iff {n q : ℕ}
    (K : Set (EuclideanSpace ℝ (Fin n))) :
    CoveredByInteriorTranslates K q ↔ CoveredByTranslates K (interior K) q

Uses 2

Statement usesCovering by interior translates · Covering by translates

TheoremThe translate covering number is the least covering count#✓fully proved

Let \(K, L \subseteq \mathbb{R}^n\) and let \(q \in \mathbb{N}\). If \(q\) is the least natural number \(r\) such that \(K\) is covered by \(r\) translates of \(L\), then the translate covering number of \(K\) by \(L\) equals \(q\).

theorem translateCoveringNumber_eq_of_isLeast {n q : ℕ}
    (K L : Set (EuclideanSpace ℝ (Fin n)))
    (h : IsLeast {r : ℕ | CoveredByTranslates K L r} q) :
    translateCoveringNumber K L = (q : WithTop ℕ)

Uses 2 · Used by 1

Statement usesCovering by translates · Translate covering number

Used byTranslate covering number of the three-dimensional cube by its interior

TheoremA least uniform bound is the Hadwiger covering number#✓fully proved

If \(q\) is the least natural number such that every convex body \(K\) in the Euclidean space \(\mathbb{R}^n\) is covered by \(q\) translates of its interior, then the Hadwiger covering number of dimension \(n\) equals \(q\).

theorem hadwigerCoveringNumber_eq_of_isLeast {n q : ℕ}
    (h : IsLeast {r : ℕ | UniformInteriorTranslateBound n r} q) :
    hadwigerCoveringNumber n = (q : WithTop ℕ)

Uses 2

Statement usesUniform bound for covering convex bodies by interior translates · Hadwiger covering number

TheoremA least uniform bound is the symmetric Hadwiger covering number#✓fully proved

If \(q\) is the least natural number such that every centrally symmetric convex body \(K\) in the Euclidean space \(\mathbb{R}^n\) is covered by \(q\) translates of its interior, then the symmetric Hadwiger covering number of dimension \(n\) equals \(q\).

theorem symmetricHadwigerCoveringNumber_eq_of_isLeast {n q : ℕ}
    (h : IsLeast {r : ℕ | UniformSymmetricInteriorTranslateBound n r} q) :
    symmetricHadwigerCoveringNumber n = (q : WithTop ℕ)

Uses 2

Statement usesUniform bound for covering centrally symmetric convex bodies by interior translates · Symmetric Hadwiger covering number

DefinitionCoordinate cube#✓fully proved

For \(n \in \mathbb{N}\), the coordinate cube is the set \([-1, 1]^n\) of points \(x\) of the Euclidean space \(\mathbb{R}^n\) with \(-1 \le x_i \le 1\) for every coordinate \(i\).

def coordinateCube (n : ℕ) : Set (EuclideanSpace ℝ (Fin n)) :=
  {x | ∀ i, x i ∈ Set.Icc (-1 : ℝ) 1}

Used by 14

Used byThe polar of the cube is the \(\ell^1\) unit ball · The Hanner cube is the coordinate cube · Covering the cube by translates of its interior needs \(2^n\) translates · The coordinate cube as an absolute-value box · Interior of the coordinate cube · The coordinate cube is centrally symmetric · The coordinate cube is a convex body · Eight translates of the interior cover the three-dimensional cube · Eight is the least number of interior translates covering the three-dimensional cube · Translate covering number of the three-dimensional cube by its interior · Affine cube · Lower bound \(2^n\) for centrally symmetric interior-translate covering · Lower bound \(2^n\) for uniform interior-translate covering · Volume of the coordinate cube

TheoremThe coordinate cube as an absolute-value box#✓fully proved

For every \(n\), the coordinate cube in \(\mathbb{R}^n\) equals the set of points \(x \in \mathbb{R}^n\) with \(|x_i| \le 1\) for every coordinate \(i\).

theorem coordinateCube_eq_absSet (n : ℕ) :
    coordinateCube n = {x : EuclideanSpace ℝ (Fin n) | ∀ i, |x i| ≤ 1}

Uses 1 · Used by 3

Statement usesCoordinate cube

Used byThe polar of the cube is the \(\ell^1\) unit ball · The Hanner cube is the coordinate cube · Volume of the coordinate cube

DefinitionAffine cube#✓fully proved

A set \(K \subseteq \mathbb{R}^n\) is an affine cube if \(K = e([-1, 1]^n)\) for some affine bijection \(e : \mathbb{R}^n \to \mathbb{R}^n\), where \([-1, 1]^n\) is the coordinate cube \(\{x \in \mathbb{R}^n : -1 \le x_i \le 1 \text{ for all } i\}\).

def IsAffineCube {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) : Prop :=
  ∃ e : EuclideanSpace ℝ (Fin n) ≃ᵃ[ℝ] EuclideanSpace ℝ (Fin n),
    K = e '' coordinateCube n

Uses 1

Statement usesCoordinate cube

TheoremInterior of the coordinate cube#✓fully proved

A point \(x \in \mathbb{R}^n\) lies in the interior of the coordinate cube \([-1, 1]^n\) if and only if \(-1 < x_i < 1\) for every coordinate \(i\).

theorem coordinateCube_interior_iff {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) :
    x ∈ interior (coordinateCube n) ↔ ∀ i, -1 < x i ∧ x i < 1

Uses 1 · Used by 3

Statement usesCoordinate cube

Used byCovering the cube by translates of its interior needs \(2^n\) translates · The coordinate cube is a convex body · Eight translates of the interior cover the three-dimensional cube

TheoremThe coordinate cube is a convex body#✓fully proved

For every \(n\), the coordinate cube \([-1, 1]^n\) in \(\mathbb{R}^n\) is a convex body: it is compact and convex, and its interior in \(\mathbb{R}^n\) is nonempty.

theorem coordinateCube_isConvexBody (n : ℕ) : IsConvexBody (coordinateCube n)

Uses 3 · Used by 2

Statement usesConvex bodies in Euclidean space · Coordinate cube

Proof usesInterior of the coordinate cube

Used byLower bound \(2^n\) for centrally symmetric interior-translate covering · Lower bound \(2^n\) for uniform interior-translate covering

TheoremThe coordinate cube is centrally symmetric#✓fully proved

For every \(n\), the coordinate cube \([-1, 1]^n\) in \(\mathbb{R}^n\) is centrally symmetric: there is a point \(c \in \mathbb{R}^n\) such that for every \(x \in \mathbb{R}^n\), \(x\) lies in the cube if and only if \(2c - x\) does.

theorem coordinateCube_isCentrallySymmetric (n : ℕ) :
    IsCentrallySymmetric (coordinateCube n)

Uses 2 · Used by 1

Statement usesCentral symmetry about some center · Coordinate cube

Used byLower bound \(2^n\) for centrally symmetric interior-translate covering

TheoremCovering the cube by translates of its interior needs \(2^n\) translates#✓fully proved

Let \(C_n = [-1, 1]^n\) be the coordinate cube in \(\mathbb{R}^n\). If \(C_n\) is contained in the union of \(q\) translates \(v_1 + \operatorname{int} C_n, \dots, v_q + \operatorname{int} C_n\) of its interior, then \(2^n \le q\).

theorem coordinateCube_coveringCount_ge_two_pow {n q : ℕ}
    (h : CoveredByInteriorTranslates (coordinateCube n) q) : 2 ^ n ≤ q

Uses 3 · Used by 3

Statement usesCovering by interior translates · Coordinate cube

Proof usesInterior of the coordinate cube

Used byEight is the least number of interior translates covering the three-dimensional cube · Lower bound \(2^n\) for centrally symmetric interior-translate covering · Lower bound \(2^n\) for uniform interior-translate covering

TheoremLower bound \(2^n\) for uniform interior-translate covering#✓fully proved

Let \(n\) and \(q\) be natural numbers. If every convex body \(K \subseteq \mathbb{R}^n\) (a compact convex set with nonempty interior) can be covered by \(q\) not necessarily distinct translates of its interior, then \(2^n \le q\).

The coordinate cube \([-1, 1]^n\) already needs \(2^n\) translates.

theorem uniformInteriorTranslateBound_ge_two_pow {n q : ℕ}
    (h : UniformInteriorTranslateBound n q) : 2 ^ n ≤ q

Uses 4 · Used by 1

Statement usesUniform bound for covering convex bodies by interior translates

Proof usesCoordinate cube · Covering the cube by translates of its interior needs \(2^n\) translates · The coordinate cube is a convex body

Used byUniform interior-translate bounds in dimension three are at least eight

TheoremUniform interior-translate bounds in dimension three are at least eight#✓fully proved

If \(q\) is a natural number such that every convex body \(K \subseteq \mathbb{R}^3\) is contained in the union of \(q\) translates of its interior \(\operatorname{int} K\), then \(8 \le q\).

theorem cubeLowerBound (q : ℕ) (h : UniformInteriorTranslateBound 3 q) : 8 ≤ q

Uses 2

Statement usesUniform bound for covering convex bodies by interior translates

Proof usesLower bound \(2^n\) for uniform interior-translate covering

TheoremLower bound \(2^n\) for centrally symmetric interior-translate covering#✓fully proved

Let \(n\) and \(q\) be natural numbers. If every centrally symmetric convex body \(K \subseteq \mathbb{R}^n\) (a compact convex set with nonempty interior that is symmetric about some point) can be covered by \(q\) not necessarily distinct translates of its interior, then \(2^n \le q\).

The coordinate cube \([-1, 1]^n\) is such a body and already needs \(2^n\) translates.

theorem symmetricInteriorTranslateBound_ge_two_pow {n q : ℕ}
    (h : UniformSymmetricInteriorTranslateBound n q) : 2 ^ n ≤ q

Uses 5

Statement usesUniform bound for covering centrally symmetric convex bodies by interior translates

Proof usesCoordinate cube · Covering the cube by translates of its interior needs \(2^n\) translates · The coordinate cube is centrally symmetric · The coordinate cube is a convex body

TheoremEight translates of the interior cover the three-dimensional cube#✓fully proved

Let \(C_3 = [-1, 1]^3\) be the coordinate cube in \(\mathbb{R}^3\). There are vectors \(v_1, \dots, v_8 \in \mathbb{R}^3\) such that \(C_3\) is contained in the union of the translates \(v_1 + \operatorname{int} C_3, \dots, v_8 + \operatorname{int} C_3\) of its interior.

theorem coordinateCube_three_coveredByInteriorTranslates :
    CoveredByInteriorTranslates (coordinateCube 3) 8

Uses 3 · Used by 1

Statement usesCovering by interior translates · Coordinate cube

Proof usesInterior of the coordinate cube

Used byEight is the least number of interior translates covering the three-dimensional cube

TheoremEight is the least number of interior translates covering the three-dimensional cube#✓fully proved

Let \(C_3 = [-1, 1]^3\) be the coordinate cube in \(\mathbb{R}^3\). Then \(8\) is the least natural number \(q\) such that \(C_3\) is contained in the union of \(q\) translates of its interior \(\operatorname{int} C_3\).

theorem coordinateCube_three_least_coveringCount :
    IsLeast {q : ℕ | CoveredByInteriorTranslates (coordinateCube 3) q} 8

Uses 4 · Used by 1

Statement usesCovering by interior translates · Coordinate cube

Proof usesCovering the cube by translates of its interior needs \(2^n\) translates · Eight translates of the interior cover the three-dimensional cube

Used byTranslate covering number of the three-dimensional cube by its interior

TheoremTranslate covering number of the three-dimensional cube by its interior#✓fully proved

Let \(C_3 = [-1, 1]^3\) be the coordinate cube in \(\mathbb{R}^3\). The translate covering number of \(C_3\) by its interior \(\operatorname{int} C_3\), the least number of translates of \(\operatorname{int} C_3\) whose union contains \(C_3\), equals \(8\).

theorem coordinateCube_three_translateCoveringNumber :
    translateCoveringNumber (coordinateCube 3) (interior (coordinateCube 3)) =
      (8 : WithTop ℕ)

Uses 4

Statement usesCoordinate cube · Translate covering number

Proof usesEight is the least number of interior translates covering the three-dimensional cube · The translate covering number is the least covering count

DefinitionIllumination by a direction#✓fully proved

Let \(K \subseteq \mathbb{R}^n\) be a set and let \(v, x \in \mathbb{R}^n\). The direction \(v\) illuminates \(x\) with respect to \(K\) when \(x\) lies on the boundary of \(K\), \(\|v\| = 1\), and \(x + tv\) lies in the interior of \(K\) for some real \(t > 0\).

def DirectionIlluminates {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n)))
    (v x : EuclideanSpace ℝ (Fin n)) : Prop :=
  x ∈ frontier K ∧ ‖v‖ = 1 ∧ ∃ t : ℝ, 0 < t ∧ x + t • v ∈ interior K

Used by 1

Used byIllumination by \(q\) directions

DefinitionIllumination by \(q\) directions#✓fully proved

A set \(K \subseteq \mathbb{R}^n\) is illuminated by \(q\) directions, for a natural number \(q\), if there are unit vectors \(v_1, \dots, v_q \in \mathbb{R}^n\) (not necessarily distinct) such that for every boundary point \(x\) of \(K\) there are an index \(i\) and a real \(t > 0\) with \(x + tv_i\) in the interior of \(K\).

def IlluminatedByDirections {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n)))
    (q : ℕ) : Prop :=
  ∃ v : Fin q → EuclideanSpace ℝ (Fin n),
    (∀ i, ‖v i‖ = 1) ∧ ∀ x ∈ frontier K, ∃ i, DirectionIlluminates K (v i) x

Uses 1 · Used by 6

Statement usesIllumination by a direction

Used byDirectional and exterior-point illumination are equivalent · Directional illumination is equivalent to covering by smaller homothets · Directional illumination number · Directional illumination is equivalent to covering by interior translates · Every convex body has a finite illumination number · Uniform covering by interior translates and uniform directional illumination

DefinitionIllumination by an external point#✓fully proved

Let \(K \subseteq \mathbb{R}^n\) be a set and let \(p, x \in \mathbb{R}^n\). The point \(p\) illuminates \(x\) with respect to \(K\) when \(p \notin K\), \(x\) lies on the boundary of \(K\), and \(p + t(x - p)\) lies in the interior of \(K\) for some real \(t > 1\); that is, the ray from \(p\) through \(x\) meets the interior of \(K\) at a point beyond \(x\).

def ExternalPointIlluminates {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n)))
    (p x : EuclideanSpace ℝ (Fin n)) : Prop :=
  p ∉ K ∧ x ∈ frontier K ∧ ∃ t : ℝ, 1 < t ∧ p + t • (x - p) ∈ interior K

Used by 1

Used byIllumination by \(q\) external points

DefinitionIllumination by \(q\) external points#✓fully proved

A set \(K \subseteq \mathbb{R}^n\) is illuminated by \(q\) external points, for a natural number \(q\), if there are points \(p_1, \dots, p_q \in \mathbb{R}^n \setminus K\) (not necessarily distinct) such that for every boundary point \(x\) of \(K\) there are an index \(i\) and a real \(t > 1\) with \(p_i + t(x - p_i)\) in the interior of \(K\).

def IlluminatedByExternalPoints {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n)))
    (q : ℕ) : Prop :=
  ∃ p : Fin q → EuclideanSpace ℝ (Fin n),
    (∀ i, p i ∉ K) ∧ ∀ x ∈ frontier K, ∃ i, ExternalPointIlluminates K (p i) x

Uses 1 · Used by 3

Statement usesIllumination by an external point

Used byDirectional and exterior-point illumination are equivalent · External-point illumination number · Uniform covering of symmetric bodies and uniform illumination by external points

DefinitionDirectional illumination number#✓fully proved

The directional illumination number of a set \(K \subseteq \mathbb{R}^n\) is the least natural number \(q\) such that \(K\) is illuminated by \(q\) directions, and \(\infty\) if there is no such \(q\).

noncomputable def directionalIlluminationNumber {n : ℕ}
    (K : Set (EuclideanSpace ℝ (Fin n))) : WithTop ℕ :=
  sInf ((fun q : ℕ ↦ (q : WithTop ℕ)) '' {q | IlluminatedByDirections K q})

Uses 1 · Used by 2

Statement usesIllumination by \(q\) directions

Used byDirectional and exterior-point illumination numbers are equal · Directional illumination number equals the interior-translate covering number

DefinitionExternal-point illumination number#✓fully proved

The external-point illumination number of a set \(K \subseteq \mathbb{R}^n\) is the least natural number \(q\) such that \(K\) is illuminated by \(q\) external points, and \(\infty\) if there is no such \(q\).

noncomputable def externalPointIlluminationNumber {n : ℕ}
    (K : Set (EuclideanSpace ℝ (Fin n))) : WithTop ℕ :=
  sInf ((fun q : ℕ ↦ (q : WithTop ℕ)) '' {q | IlluminatedByExternalPoints K q})

Uses 1 · Used by 1

Statement usesIllumination by \(q\) external points

Used byDirectional and exterior-point illumination numbers are equal

TheoremTwo equivalent formulations of Hadwiger's covering conjecture#●ready to prove

The following statements are equivalent: for every \(n \ge 1\), every convex body \(K \subseteq \mathbb{R}^n\) is covered by at most \(2^n\) homothets \(v_i + r_i K\) with \(v_i \in \mathbb{R}^n\) and \(0 < r_i < 1\); and for every \(n \ge 1\), every convex body \(K \subseteq \mathbb{R}^n\) is covered by \(2^n\) translates of its interior \(\operatorname{int} K\), repetitions allowed.

theorem_wanted homothetInteriorTranslateFormulationsEquivalent :
    (∀ n : ℕ, 0 < n → ∀ K : Set (EuclideanSpace ℝ (Fin n)), IsConvexBody K →
      ∃ q : ℕ, q ≤ 2 ^ n ∧ CoveredBySmallerPositiveHomothets K q) ↔
      ∀ n : ℕ, 0 < n → UniformInteriorTranslateBound n (2 ^ n)

Sources

• Bezdek and Khan, arXiv:1602.06040v2, introduction; Arman, Kaire and Prymak, arXiv:2510.25968v3, introduction.

Uses 3

Statement usesCovering by smaller positive homothets · Convex bodies in Euclidean space · Uniform bound for covering convex bodies by interior translates

TheoremPapadoperakis's bound for Hadwiger's covering problem in dimension 3#●ready to prove

Every convex body \(K \subseteq \mathbb{R}^3\) is covered by \(16\) translates of its interior \(\operatorname{int} K\), repetitions allowed.

theorem_wanted papadoperakis1999UpperBound : UniformInteriorTranslateBound 3 16

Sources

• Papadoperakis (1999), reported in Arman, Bondarenko and Prymak, arXiv:2404.00547v1, introduction.

Uses 1

Statement usesUniform bound for covering convex bodies by interior translates

TheoremPrymak's bound for Hadwiger's covering problem in dimension 3#●ready to prove

Every convex body \(K \subseteq \mathbb{R}^3\) is covered by \(14\) translates of its interior \(\operatorname{int} K\), repetitions allowed.

theorem_wanted prymak2023UpperBound : UniformInteriorTranslateBound 3 14

Sources

• Prymak (2023), arXiv:2112.10698; reported in Arman, Bondarenko and Prymak, arXiv:2404.00547v1, introduction.

Uses 1

Statement usesUniform bound for covering convex bodies by interior translates

TheoremLassak's theorem for centrally symmetric bodies in dimension 3#●ready to prove

The number \(8\) is the least natural number \(q\) such that every centrally symmetric convex body \(K \subseteq \mathbb{R}^3\) is covered by \(q\) translates of its interior \(\operatorname{int} K\), repetitions allowed. Here \(K\) is centrally symmetric when there is a point \(c\) with \(x \in K\) if and only if \(2c - x \in K\).

theorem_wanted lassak1984SymmetricExactValue :
  IsLeast {q : ℕ | UniformSymmetricInteriorTranslateBound 3 q} 8

Sources

• Lassak (1984), reported in Arman, Bondarenko and Prymak, arXiv:2404.00547v1, introduction.

Uses 1

Statement usesUniform bound for covering centrally symmetric convex bodies by interior translates

TheoremDirectional and exterior-point illumination are equivalent#●ready to prove

Let \(n \ge 1\), let \(K \subseteq \mathbb{R}^n\) be a convex body and let \(q\) be a natural number. Then some \(q\) unit vectors \(v_1, \dots, v_q\) illuminate \(K\) if and only if some \(q\) points \(p_1, \dots, p_q\) outside \(K\) illuminate \(K\). Here the vectors illuminate \(K\) when every boundary point \(x\) of \(K\) has an \(i\) and a \(t > 0\) with \(x + t v_i\) in the interior of \(K\), and the points illuminate \(K\) when every boundary point \(x\) of \(K\) has an \(i\) and a \(t > 1\) with \(p_i + t (x - p_i)\) in the interior of \(K\).

theorem_wanted directionalExternalFormulationsEquivalent :
    ∀ n : ℕ, 0 < n → ∀ K : Set (EuclideanSpace ℝ (Fin n)), IsConvexBody K →
      ∀ q : ℕ, IlluminatedByDirections K q ↔ IlluminatedByExternalPoints K q

Sources

• Bezdek and Khan, arXiv:1602.06040v2, introduction.

Uses 3

Statement usesIllumination by \(q\) directions · Illumination by \(q\) external points · Convex bodies in Euclidean space

TheoremDirectional illumination is equivalent to covering by smaller homothets#●ready to prove

Let \(n \ge 1\), let \(K \subseteq \mathbb{R}^n\) be a convex body and let \(q\) be a natural number. Then some \(q\) unit vectors illuminate \(K\) if and only if \(K\) is covered by \(q\) homothets \(v_1 + r_1 K, \dots, v_q + r_q K\) with \(v_i \in \mathbb{R}^n\) and \(0 < r_i < 1\), repetitions allowed.

theorem_wanted directionalHomothetFormulationsEquivalent :
    ∀ n : ℕ, 0 < n → ∀ K : Set (EuclideanSpace ℝ (Fin n)), IsConvexBody K →
      ∀ q : ℕ, IlluminatedByDirections K q ↔ CoveredBySmallerPositiveHomothets K q

Sources

• Bezdek and Khan, arXiv:1602.06040v2, introduction.

Uses 3

Statement usesCovering by smaller positive homothets · Illumination by \(q\) directions · Convex bodies in Euclidean space

TheoremDirectional illumination is equivalent to covering by interior translates#●ready to prove

Let \(n \ge 1\), let \(K \subseteq \mathbb{R}^n\) be a convex body and let \(q\) be a natural number. Then some \(q\) unit vectors illuminate \(K\) if and only if \(K\) is covered by \(q\) translates \(v_1 + \operatorname{int} K, \dots, v_q + \operatorname{int} K\) of its interior, repetitions allowed.

theorem_wanted directionalInteriorFormulationsEquivalent :
    ∀ n : ℕ, 0 < n → ∀ K : Set (EuclideanSpace ℝ (Fin n)), IsConvexBody K →
      ∀ q : ℕ, IlluminatedByDirections K q ↔ CoveredByInteriorTranslates K q

Sources

• Arman, Kaire and Prymak, arXiv:2510.25968v3, introduction.

Uses 3

Statement usesCovering by interior translates · Illumination by \(q\) directions · Convex bodies in Euclidean space

TheoremDirectional and exterior-point illumination numbers are equal#●ready to prove

For every \(n \ge 1\) and every convex body \(K \subseteq \mathbb{R}^n\), the directional illumination number of \(K\) equals its exterior-point illumination number. These are the least \(q\) such that some \(q\) unit vectors, respectively some \(q\) points outside \(K\), illuminate \(K\), with the value \(\infty\) when no finite family does.

theorem_wanted directionalExternalIlluminationNumbersEqual (n : ℕ) (hn : 0 < n)
    (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsConvexBody K) :
    directionalIlluminationNumber K = externalPointIlluminationNumber K

Sources

• Bezdek and Khan, arXiv:1602.06040v2, introduction; follows from its finite-count equivalence, whose Lean proof is also requested here.

Uses 3

Statement usesConvex bodies in Euclidean space · Directional illumination number · External-point illumination number

TheoremDirectional illumination number equals the interior-translate covering number#●ready to prove

For every \(n \ge 1\) and every convex body \(K \subseteq \mathbb{R}^n\), the directional illumination number of \(K\) equals the least \(q\) such that \(K\) is covered by \(q\) translates of its interior \(\operatorname{int} K\). Both sides take the value \(\infty\) when no finite family exists.

theorem_wanted directionalInteriorCoveringNumbersEqual (n : ℕ) (hn : 0 < n)
    (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsConvexBody K) :
    directionalIlluminationNumber K = translateCoveringNumber K (interior K)

Sources

• Arman, Kaire and Prymak, arXiv:2510.25968v3, introduction; follows from the finite-count equivalence, whose Lean proof is also requested here.

Uses 3

Statement usesConvex bodies in Euclidean space · Directional illumination number · Translate covering number

TheoremEvery convex body has a finite illumination number#●ready to prove

For every \(n \ge 1\) and every convex body \(K \subseteq \mathbb{R}^n\) there is a least natural number \(q\) such that some \(q\) unit vectors \(v_1, \dots, v_q\) illuminate \(K\): every boundary point \(x\) of \(K\) has an \(i\) and a \(t > 0\) with \(x + t v_i\) in the interior of \(K\).

theorem_wanted illuminationFiniteMinimum :
    ∀ n : ℕ, 0 < n → ∀ K : Set (EuclideanSpace ℝ (Fin n)), IsConvexBody K →
      ∃ q : ℕ, IsLeast {q : ℕ | IlluminatedByDirections K q} q

Sources

• Arman, Kaire and Prymak, arXiv:2510.25968v3, introduction's illumination-number definition; finite existence is the standard compact-convex-body qualification.

Uses 2

Statement usesIllumination by \(q\) directions · Convex bodies in Euclidean space

TheoremUniform covering by interior translates and uniform directional illumination#●ready to prove

For integers \(n \ge 1\) and \(q \ge 0\), every convex body in \(\mathbb{R}^n\) (a compact convex set with nonempty interior) can be covered by \(q\) translates of its interior if and only if every convex body \(K\) in \(\mathbb{R}^n\) is illuminated by \(q\) directions: there are unit vectors \(v_1, \dots, v_q\) such that each boundary point \(x\) of \(K\) has some \(i\) and some \(t > 0\) with \(x + t v_i\) in the interior of \(K\).

theorem_wanted uniformDirectionalIlluminationInterpretation (n : ℕ) (hn : 0 < n) (q : ℕ) :
    UniformInteriorTranslateBound n q ↔
      ∀ K : Set (EuclideanSpace ℝ (Fin n)), IsConvexBody K → IlluminatedByDirections K q

Sources

• Arman, Kaire and Prymak, arXiv:2510.25968v3, introduction; follows from the finite-count equivalence, whose Lean proof is also requested here.

Uses 3

Statement usesIllumination by \(q\) directions · Convex bodies in Euclidean space · Uniform bound for covering convex bodies by interior translates

TheoremUniform covering of symmetric bodies and uniform illumination by external points#●ready to prove

For integers \(n \ge 1\) and \(q \ge 0\), every centrally symmetric convex body in \(\mathbb{R}^n\) (a compact convex set with nonempty interior that is symmetric about some point) can be covered by \(q\) translates of its interior if and only if every centrally symmetric convex body \(K\) in \(\mathbb{R}^n\) is illuminated by \(q\) external points: there are points \(p_1, \dots, p_q\) outside \(K\) such that each boundary point \(x\) of \(K\) has some \(i\) and some \(t > 1\) with \(p_i + t(x - p_i)\) in the interior of \(K\).

theorem_wanted uniformSymmetricExternalIlluminationInterpretation (n : ℕ) (hn : 0 < n) (q : ℕ) :
    UniformSymmetricInteriorTranslateBound n q ↔
      ∀ K : Set (EuclideanSpace ℝ (Fin n)), IsConvexBody K → IsCentrallySymmetric K →
        IlluminatedByExternalPoints K q

Sources

• Arman, Kaire and Prymak, arXiv:2510.25968v3, introduction, and Bezdek and Khan, arXiv:1602.06040v2, introduction; follows from the two finite-count equivalences.

Uses 4

Statement usesIllumination by \(q\) external points · Central symmetry about some center · Convex bodies in Euclidean space · Uniform bound for covering centrally symmetric convex bodies by interior translates

34 fully proved12 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.