OAI/NumberTheory/TwoPoint/Bounds/ActualWordInputs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A finite list of every literal in a weighted word: the padding state at each endpoint, its centered-prime tests, and every occurrence in the prohibited-site DNFs. Equal primes share one residue coordinate.

  1. abbrev OAI.TwoPointCorrelations.ActualWordInput line 15
  2. def OAI.TwoPointCorrelations.actualWordInputEquiv line 20
  3. def OAI.TwoPointCorrelations.actualWordLiterals line 24
  4. def OAI.TwoPointCorrelations.actualWordQIndex line 34
  5. def OAI.TwoPointCorrelations.actualWordPIndex line 39
  6. def OAI.TwoPointCorrelations.actualWordBadIndex line 43
  7. def OAI.TwoPointCorrelations.actualWordIntegerBits line 48
  8. lemma OAI.TwoPointCorrelations.actualWordQIndex_eval line 57
  9. lemma OAI.TwoPointCorrelations.actualWordBadIndex_eval line 67
  10. lemma OAI.TwoPointCorrelations.actualWordPIndex_eval line 78