OAI/NumberTheory/TwoPoint/Walks/TupleSlice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact splitting of a prime tuple into the removed and retained supplies in the quantitative centering expansion.

  1. lemma OAI.TwoPointCorrelations.indexed_prime_product_injective line 14
  2. def OAI.TwoPointCorrelations.primeTupleSlice line 36
  3. lemma OAI.TwoPointCorrelations.primeTupleSlice_injective line 39
  4. lemma OAI.TwoPointCorrelations.primeTupleSlice_mass line 46
  5. lemma OAI.TwoPointCorrelations.primeTupleSlice_pos line 61
  6. lemma OAI.TwoPointCorrelations.primeTupleSlice_lower line 67
  7. lemma OAI.TwoPointCorrelations.primeTupleSlice_split_sum line 78