OAI/NumberTheory/TwoPoint/Walks/CanonicalComplexPrefix.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Canonical directed complex prefix estimate with all boundary terms explicit.

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