OAI/NumberTheory/TwoPoint/Halasz/HalaszMomentSampling.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Fourier sampling of the second complete-system moment.
- theorem
OAI.TwoPointCorrelations.halasz_moment_samplingline 12