OAI/NumberTheory/Ostmann/Construction/HalfListTest.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Construction.FinitePrior.pair_mean line 15
  2. theorem OAI.Ostmann.Construction.FinitePrior.mean_mul_const line 20
  3. theorem OAI.Ostmann.Construction.FinitePrior.mean_const_mul line 25
  4. theorem OAI.Ostmann.Construction.FinitePrior.pair_mean_product line 33
  5. def OAI.Ostmann.Construction.primeSourceTestMean line 41
  6. def OAI.Ostmann.Construction.primeGroupTestMean line 44
  7. def OAI.Ostmann.Construction.giantTestMean line 49
  8. def OAI.Ostmann.Construction.halfListTest line 52
  9. abbrev OAI.Ostmann.Construction.HalfListSample line 57
  10. def OAI.Ostmann.Construction.halfListPrior line 61
  11. def OAI.Ostmann.Construction.halfListTupleTest line 67
  12. theorem OAI.Ostmann.Construction.halfListTest_eq_tuple_mean line 77
  13. theorem OAI.Ostmann.Construction.primeSourceTestMean_on_summand line 121
  14. theorem OAI.Ostmann.Construction.primeGroupTestMean_on_summand line 130
  15. theorem OAI.Ostmann.Construction.halfListTest_on_summand line 143