OAI/NumberTheory/TwoPoint/Bounds/LiouvilleDivisorExtraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact partial-centering substitution n=u*v. Only u must be a unit modulo l; the progression class and the removed product may be nonunits.

  1. lemma OAI.TwoPointCorrelations.unit_progression_cancel line 14
  2. lemma OAI.TwoPointCorrelations.liouville_pair_dilate line 22
  3. lemma OAI.TwoPointCorrelations.liouville_progression_dilate line 31
  4. def OAI.TwoPointCorrelations.partialLiouvilleProfile line 41
  5. lemma OAI.TwoPointCorrelations.partialLiouvilleProfile_prefix line 47
  6. lemma OAI.TwoPointCorrelations.natDivisibilityIndicator_mul line 60