OAI/NumberTheory/TwoPoint/Bounds/ProgressionCompressionGate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Freeze the ambient progression condition within each residue class before applying the affine-origin compression estimate.

  1. lemma OAI.TwoPointCorrelations.progressionEdgeGate_function line 13
  2. lemma OAI.TwoPointCorrelations.primeBlockCompression_progression_freeze line 19