OAI/NumberTheory/TwoPoint/Bounds/ProgressionBlockTesting.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Combine the residue classes of block origins. The progression gate is frozen in each class, and every block retains its ambient endpoint cuts.

  1. def OAI.TwoPointCorrelations.ambientLiouvilleBlockForm line 15
  2. lemma OAI.TwoPointCorrelations.ambientLiouvilleBlockForm_eq line 24
  3. lemma OAI.TwoPointCorrelations.ambientLiouvilleBlockForm_progression line 39
  4. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_progression_block_testing_uniform line 57
  5. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_progression_block_testing line 114