OAI/NumberTheory/Ostmann/Arithmetic/HistoryGiantReferenceMeanMetadata.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryGiantReferenceMean.drawHistory_root_small line 14
2. theorem OAI.Ostmann.Arithmetic.HistoryGiantReferenceMean.drawHistory_root_frequency line 19
3. theorem OAI.Ostmann.Arithmetic.HistoryGiantReferenceMean.drawHistory_internalOccurrences line 24
4. theorem OAI.Ostmann.Arithmetic.HistoryGiantReferenceMean.drawHistory_compensationProduct line 31
5. theorem OAI.Ostmann.Arithmetic.HistoryGiantReferenceMean.source_draw_root_mass line 38
6. theorem OAI.Ostmann.Arithmetic.HistoryGiantReferenceMean.source_draw_internal_mass line 47
7. theorem OAI.Ostmann.Arithmetic.HistoryGiantReferenceMean.prime_reference_cells line 56
8. theorem OAI.Ostmann.Arithmetic.HistoryGiantReferenceMean.mixed_reference_cells line 64