Revision #3381 → #3985 · back to history
modifiedSphere packing00052e219c72
| Field | From #3381 | To #3985 |
|---|
| note | No declaration in Mathlib captures the notion of a sphere packing (an arrangement of non-overlapping balls in a space). | Mathlib has no declaration formalizing the notion of a sphere packing (arrangement of non-overlapping balls in a space). |
modifiedPacking densityf9e1107726e8
| Field | From #3381 | To #3985 |
|---|
| note | Mathlib has no notion of packing density (proportion of space filled by a packing). | Mathlib has no notion of packing density (proportion of space occupied by the packing). |
modifiedDensest packing in 3D ≈ 74%7191d5f29133
| Field | From #3381 | To #3985 |
|---|
| note | No formalization of the optimal 3D sphere packing density (π/√18) exists in Mathlib. | The optimal 3D sphere-packing density π/√18 (Kepler conjecture) is not formalized in Mathlib. |
modifiedRandom packing density ≈ 63.5%6bc2a8811716
| Field | From #3381 | To #3985 |
|---|
| note | Random close packing density is an empirical / physical statement absent from Mathlib. | Random close packing density is an empirical/physical claim absent from Mathlib. |
modifiedLattice arrangemente9c7733e0046
| Field | From #3381 | To #3985 |
|---|
| note | Mathlib defines `ZLattice` (a discrete cocompact ℤ-submodule of a real vector space) which underlies lattice packings, but does not formalize lattice packings themselves. | Mathlib defines `ZLattice` (a discrete cocompact ℤ-submodule of a real vector space) underlying lattice packings, but does not formalize lattice packings themselves. |
modifiedOther common lattice packing densities240ecaa45211
| Field | From #3381 | To #3985 |
|---|
| note | Mathlib does not compute packing densities for common lattices. | Mathlib does not compute packing densities for the standard lattices. |
modifiedAsymptotic bounds on densest latticefd08832840ad
| Field | From #3381 | To #3985 |
|---|
| note | Asymptotic Minkowski–Hlawka / Kabatyanskii–Levenshtein bounds are not in Mathlib. | Asymptotic Minkowski–Hlawka and Kabatyanskii–Levenshtein bounds are not in Mathlib. |
modifiedContact graph of a packingcc681a1877f0
| Field | From #3381 | To #3985 |
|---|
| note | Contact graphs of sphere packings are not defined in Mathlib (though `SimpleGraph` is). | Contact graphs of sphere packings are not defined in Mathlib (although `SimpleGraph` is). |
modifiedSphere packing and error-correcting codesf7814cac1d1f
| Field | From #3381 | To #3985 |
|---|
| note | Mathlib has no theory linking sphere packings to error-correcting codes (no Hamming/linear-code packing infrastructure found). | Mathlib has no theory linking sphere packings to error-correcting codes. |
addedCircle packingfc6efc23de86
addedHyperbolic space447c6b17e1c5
addedPoisson summation applied to sphere packing875f97a79c63
addedFourier transform61ee2c406738
addedLaplace transform64d79db001dc
addedFord circles733cd0201e4d
addedHamming distance / Hamming ballsa445a7af515e
addedLinear codes ↔ lattice packings43b57798f83e
addedBinary Golay code and Leech latticea411b8f45f67