OAI/NumberTheory/EgyptianFractions/RationalArcGeometry.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Checked rational major/minor arc geometry
This aggregate joins the reduced Dirichlet, finite rational-union, and periodic normalized-center interfaces. It also includes logarithmic scalar error budgets. It asserts no prime-distribution or exponential-sum cancellation theorem.
This file declares nothing itself. It gathers the 5 imports below, so a file that imports it gets all of them.