OAI/NumberTheory/TwoPoint/Bounds/PrimeMatrixResidues.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Discharge residue periodicity for the literal prime-family matrix weights.

  1. theorem OAI.TwoPointCorrelations.primeClosedPair_residue_congr line 13
  2. lemma OAI.TwoPointCorrelations.maskedSignedIntegerWeight_pairs line 40
  3. lemma OAI.TwoPointCorrelations.scalarWalkProduct_pairs line 51