OAI/NumberTheory/JointDickman/Counting/DilatedWindowEnergy.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Exact normalization under a fixed dilation of short windows
- theorem
OAI.JointDickman.normalized_dilate_energyline 9