OAI/NumberTheory/TwoPoint/Walks/RetainedNumericalPrefix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Reindex the retained prefix by the original numerical divisors, with no tuple-representation multiplicity.

  1. def OAI.TwoPointCorrelations.retainedNumericalEdge line 14
  2. lemma OAI.TwoPointCorrelations.retainedPrimeEdge_eq_numerical line 25
  3. lemma OAI.TwoPointCorrelations.retained_tuple_sum_eq_numerical line 34
  4. theorem OAI.TwoPointCorrelations.retainedPrimePrefix_eq_numerical line 56
  5. lemma OAI.TwoPointCorrelations.positivePrefix_real_denominator_le line 69