OAI/NumberTheory/TwoPoint/Bounds/PrimeLiteralEncoding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Canonical residue coordinates for the prime-and-offset literals occurring in a weighted matrix word. Repeated tests share one prime coordinate, and may have different offsets.

  1. def OAI.TwoPointCorrelations.primeResidueModuli line 16
  2. def OAI.TwoPointCorrelations.primeLiteralCoordinate line 19
  3. def OAI.TwoPointCorrelations.primeLiteralTest line 23
  4. lemma OAI.TwoPointCorrelations.primeResidueModuli_coordinate line 28
  5. lemma OAI.TwoPointCorrelations.primeLiteral_integer_input line 33
  6. lemma OAI.TwoPointCorrelations.primeResidueModuli_prime line 45
  7. lemma OAI.TwoPointCorrelations.primeResidueModuli_coprime line 49
  8. lemma OAI.TwoPointCorrelations.primeResidueModuli_bound line 59
  9. lemma OAI.TwoPointCorrelations.primePool_card_bound line 63