OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkReferenceFrequencyFamilyRoots.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.RootFrequencyIndex line 12
2. abbrev OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.RootReferenceFamily line 15
3. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.RootPresent line 23
4. instance OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rootPresentFintype line 26
5. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rootSelected line 32
6. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rootLeftHistory line 36
7. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rootRightHistory line 40
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rootLeftHistory_supported line 44
9. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rootRightHistory_supported line 47
10. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.root_supported_assignment_injective line 50
11. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rootOptionValue line 70
12. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rootOptionValue_present line 74
13. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.sum_rootOptionValue_eq_present line 82
14. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.root_reference_frequency_average_eventually line 98