OAI/NumberTheory/JointDickman/Counting/ShortAffineLimit.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Iterated short averages from a uniform affine spectral budget
- theorem
OAI.JointDickman.shortAverage_iterated_affineline 11