OAI/NumberTheory/Ostmann/Arithmetic/MovingSampleValues.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The labelled sampler evaluates to the actual natural prime sampler

  1. def OAI.Ostmann.movingSlotValues line 11
  2. def OAI.Ostmann.movingCompensationValues line 16
  3. def OAI.Ostmann.MovingSampleSlots.values line 21
  4. theorem OAI.Ostmann.movingNaturalProduct_append line 27
  5. theorem OAI.Ostmann.movingSlotValues_flatten line 32
  6. theorem OAI.Ostmann.movingSlotValues_append line 43
  7. theorem OAI.Ostmann.movingCompensationValues_product line 53
  8. theorem OAI.Ostmann.buildMovingSlotData_frequency line 64