OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkPriorGridTuple.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.BulkPrimeTuple line 17
  2. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkTupleRetained line 21
  3. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkTupleWeight line 24
  4. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkGridMean line 27
  5. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkProductPrior line 30
  6. def OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkRetainedTupleEquiv line 35
  7. theorem OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkProductPrior_cmean_eq_retained_grid line 45
  8. theorem OAI.Ostmann.Arithmetic.HistoryBulkPriorGrid.bulkGridMean_eq_assigned line 65