OAI/NumberTheory/TwoPoint/Bounds/MaskedWeightPeriodicity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The literal masked arithmetic weights depend only on the finite prime residues.

  1. lemma OAI.TwoPointCorrelations.centeredTuple_eq_of_prime_residues line 13
  2. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.prohibitedSite_congr line 23
  3. lemma OAI.TwoPointCorrelations.maskedSignedIntegerWeight_residue_congr line 37
  4. lemma OAI.TwoPointCorrelations.scalarWalkProduct_residue_congr line 92