OAI/NumberTheory/Ostmann/Construction/LogCellPrior.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Construction.LogCellSample line 10
2. theorem OAI.Ostmann.Construction.logCell_sample_sum line 12
3. def OAI.Ostmann.Construction.logCellPrior line 16
4. theorem OAI.Ostmann.Construction.logCellPrior_mass line 21
5. theorem OAI.Ostmann.Construction.logCellSample_prime line 28
6. theorem OAI.Ostmann.Construction.logCellSample_not_deleted line 31
7. theorem OAI.Ostmann.Construction.logCellPrior_mass_le line 34