OAI/NumberTheory/Ostmann/Construction/InitialSourceChoice.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Construction.bulkPrimeBand line 13
  2. def OAI.Ostmann.Construction.bulkPrimeSource line 16
  3. structure OAI.Ostmann.Construction.InitialSourceChoice line 20
  4. def OAI.Ostmann.Construction.InitialSourceChoice.scale line 37
  5. def OAI.Ostmann.Construction.InitialSourceChoice.giant line 40
  6. def OAI.Ostmann.Construction.InitialSourceChoice.bulk line 43
  7. def OAI.Ostmann.Construction.InitialSourceChoice.auxiliary line 46
  8. def OAI.Ostmann.Construction.InitialSourceChoice.sources line 49
  9. def OAI.Ostmann.Construction.InitialSourceChoice.test line 52
  10. def OAI.Ostmann.Construction.InitialSourceChoice.statistic line 56
  11. theorem OAI.Ostmann.Construction.InitialSourceChoice.auxiliary_balanced line 59
  12. theorem OAI.Ostmann.Construction.InitialSourceChoice.test_summable line 63