OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseFromPolynomial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform logarithmic phase prefixes from the normalized polynomial estimate, with one common boundary error for both short-variable scales.

  1. theorem OAI.TwoPointCorrelations.halasz_phase_from_polynomial line 12