HalaszSharpNearEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Near-center energy with the exceptional prefix density squared. The phase-shaped approximation is applied to the typical coefficient itself, before the Fourier energy is integrated.

lemma OAI.TwoPointCorrelations.halasz_sharp_near_energy line 13