OAI/NumberTheory/Ostmann/Construction/ScheduledFrequencyBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The concrete rounded frequency family and its finite counting cost

  1. theorem OAI.Ostmann.transferErrorScale_monotone line 13
  2. theorem OAI.Ostmann.naturalTransferCutoff_monotone line 21
  3. theorem OAI.Ostmann.transferFrequencyRange_mono line 26
  4. theorem OAI.Ostmann.scheduledFrequencyIndex_card_le line 30
  5. theorem OAI.Ostmann.scheduledFrequencyIndex_pair_card_bound line 59