HalaszTypicalPrefix.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform centered typical prefixes. The distance and frequency range are still imposed at the original cutoff, while the typical bands remain fixed as the prefix varies.

theorem OAI.TwoPointCorrelations.halasz_typical_centered_prefix line 15