OAI/NumberTheory/TwoPoint/Halasz/HalaszClassicalMeanValue.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The iterated classical Vinogradov mean-value estimate, with an explicit geometric defect and explicit constants at every finite scale.

  1. theorem OAI.TwoPointCorrelations.halasz_classical_mean_value line 11