OAI/NumberTheory/Ostmann/Construction/PrimeSources.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.Construction.PrimeSource line 10
2. abbrev OAI.Ostmann.Construction.PrimeSource.Sample line 15
3. abbrev OAI.Ostmann.Construction.SourceFamily line 16
4. def OAI.Ostmann.Construction.sourceMass line 18
5. theorem OAI.Ostmann.Construction.sourceMass_nonneg line 22
6. def OAI.Ostmann.Construction.dependentProductPrior line 29
7. theorem OAI.Ostmann.Construction.dependentProductPrior_cmean line 36
8. abbrev OAI.Ostmann.Construction.SourceAssignment line 45
9. def OAI.Ostmann.Construction.assignmentPrior line 48
10. def OAI.Ostmann.Construction.assignedSlots line 52
11. theorem OAI.Ostmann.Construction.assignedSlots_mass line 56
12. theorem OAI.Ostmann.Construction.assignedSlots_prime line 66
13. theorem OAI.Ostmann.Construction.assignedSlots_length line 73