OAI/NumberTheory/TwoPoint/Halasz/HalaszQuantitativeMeanValue.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The one quantitative complete-system estimate used by the subsequent logarithmic phase argument. Both the defect and the constant are explicit.

  1. theorem OAI.TwoPointCorrelations.halasz_quantitative_mean_value line 10