Low-discrepancy quasi-uniform digital nets in every dimension: manuscript, Lean formalization and blueprint
LaTeX source, reproduction scripts, Lean 4 / Mathlib formalization (616 compared theorems, accepted by Comparator with the Lean and NanoDa kernels), leanblueprint and interactive explainers of the manuscript "Low-discrepancy quasi-uniform digital nets in every dimension" (version 1), which constructs, for every dimensi...