OAI/NumberTheory/TwoPoint/Halasz/HalaszTypicalNearActual.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual typical-band near energy retains exponential saving, with no discarded-density term in the amplitude.

  1. theorem OAI.TwoPointCorrelations.halasz_typical_near_actual line 16