Packings and coverings

Optimal arrangements of congruent bodies in space and the smallest sets or fewest translates needed to cover given families of shapes.

• Goodman–Goodman circle covering theorem
• Hadwiger covering and illumination problem
• Kepler conjecture
• Lebesgue's universal covering problem
• Moser's worm problem
• Sphere packing in four dimensions

TheoremKlartag's lattice packing theorem#●ready to prove

There is a real constant \(c > 0\) such that for every integer \(n \ge 1\) there is a linear map \(\varphi : \mathbb{R}^n \to \mathbb{R}^n\) for which the ellipsoid \(E = \varphi(B)\), the image of the open Euclidean unit ball \(B\) about the origin, has volume exactly \(c n^2\) and the origin is the only point of \(E\) whose coordinates are all integers.

The map \(\varphi\) is not required to be invertible; a degenerate \(\varphi\) would give volume \(0\).

public theorem_wanted klartag_packing : ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 0 < n →
    let V := EuclideanSpace ℝ (Fin n)
    ∃ φ : V →ₗ[ℝ] V, let E := φ '' Metric.ball (0 : V) 1
      (MeasureTheory.volume E : EReal) = c * n ^ 2 ∧
      {v ∈ E | ∀ i, v i ∈ Set.range ((↑) : ℤ → ℝ)} = {0}

Sources

-. Problem klartag_packing of the lean-eval benchmark.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.