OAI/NumberTheory/Ostmann/Construction/SpectatorBulkScale.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The even bulk size and the accumulated giant loss in Section 9

  1. def OAI.Ostmann.spectatorBulkCount line 16
  2. theorem OAI.Ostmann.spectatorBulkCount_even line 19
  3. theorem OAI.Ostmann.spectatorBulkCount_lower line 22
  4. theorem OAI.Ostmann.spectatorBulkCount_upper line 29
  5. theorem OAI.Ostmann.spectatorBulkCount_half line 36
  6. theorem OAI.Ostmann.spectatorBulkCount_tendsto line 41
  7. theorem OAI.Ostmann.spectatorBulkCount_iteration_budget line 50