OAI/NumberTheory/TwoPoint/Bounds/ProgressionEdgeGate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The progression restriction is symmetric in the two endpoints and is fixed while the block origin moves through one residue class.

  1. def OAI.TwoPointCorrelations.progressionEdgeGate line 11
  2. lemma OAI.TwoPointCorrelations.progressionEdgeGate_symmetric line 16
  3. lemma OAI.TwoPointCorrelations.progressionEdgeGate_add_mul line 20
  4. lemma OAI.TwoPointCorrelations.progressionEdgeGate_freeze line 32