OAI/NumberTheory/TwoPoint/Bounds/QualitativeCenteringTotal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sum every actual logarithmic bin, retaining arbitrary unit-disk phase weights and the exact padding and tuple normalizers.

  1. theorem OAI.TwoPointCorrelations.qualitative_canonical_nonraw_total line 14