OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSourceDisintegrationDefs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.NonbulkPosition line 13
2. abbrev OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.NonbulkSample line 16
3. def OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.nonbulkPrior line 19
4. def OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.bulkPrior line 23
5. def OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.bulkSampleEquiv line 31
6. def OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.coordinateEquiv line 36
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.coordinateEquiv_nonbulk_apply line 59
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.coordinateEquiv_bulk_apply line 63
9. theorem OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.coordinateEquiv_bulk_val line 67
10. theorem OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.coordinateEquiv_bulk_mass line 71