OAI/NumberTheory/TwoPoint/Halasz/HalaszEnergyDiagonal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Diagonal pairs in the long variables retain a full copy of the short-variable energy for each long tuple.

  1. theorem OAI.TwoPointCorrelations.halasz_energy_diagonal_lower line 12