OAI/NumberTheory/TwoPoint/Walks/CanonicalComplexTesting.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The canonical spectral estimate applied to two arbitrary complex sequences. The short-range hypothesis only selects the ten color tests.

  1. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_complex_blocks line 13