OAI/NumberTheory/TwoPoint/Walks/TupleCenterExpansion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact expansion indexed by the set of prime supplies replaced by reciprocal constants. The original tuple and all progression tests are retained.

  1. lemma OAI.TwoPointCorrelations.indexed_indicator_product line 14
  2. lemma OAI.TwoPointCorrelations.tupleCenter_expansion line 30
  3. lemma OAI.TwoPointCorrelations.tupleCenter_expansion_zero line 47
  4. lemma OAI.TwoPointCorrelations.tupleCenter_nonraw_expansion line 56
  5. lemma OAI.TwoPointCorrelations.centeredTuple_nat_eq line 79