OAI/NumberTheory/TwoPoint/Walks/CanonicalTupleSlices.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual centered bands satisfy every arithmetic support condition used by quantitative partial centering, including nonunit progression classes.

  1. lemma OAI.TwoPointCorrelations.retainedPrimeDivisor_coprime_of_primes line 14
  2. lemma OAI.TwoPointCorrelations.centeredPrimeBands_coprime line 20
  3. lemma OAI.TwoPointCorrelations.paddingPrimeDivisor_coprime line 26
  4. lemma OAI.TwoPointCorrelations.paddingPrimeDivisor_coprime_centered line 34
  5. lemma OAI.TwoPointCorrelations.partial_tuple_unit line 46
  6. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_tuple_slices line 57