OAI/NumberTheory/Ostmann/Construction/IntegerIntervalCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Identifying actual integer sets with the interval coordinates of the sieve

  1. def OAI.Ostmann.integerIntervalIndices line 9
  2. def OAI.Ostmann.integerIntervalPoint line 12
  3. theorem OAI.Ostmann.integerIntervalPoint_injective line 14
  4. theorem OAI.Ostmann.integerIntervalIndices_image line 21
  5. theorem OAI.Ostmann.integerIntervalIndices_card line 39
  6. theorem OAI.Ostmann.averagedCoordinates_image line 46
  7. theorem OAI.Ostmann.integerIntervalIndices_average line 54
  8. theorem OAI.Ostmann.restricted_integer_energy_budget line 76