OAI/NumberTheory/TwoPoint/Halasz/HalaszTypicalShortEnergySharp.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The short-window energy of the literal typical coefficient, before any exceptional integers are removed. The original distance scale and frequency height are unchanged.

  1. theorem OAI.TwoPointCorrelations.halasz_typical_short_energy_sharp line 17