OAI/NumberTheory/Ostmann/Arithmetic/HistoryProductWindowsCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.matches_metadata_fin_sum line 12
2. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.small_log_error line 20
3. def OAI.Ostmann.Arithmetic.HistoryProductWindows.realProduct line 43
4. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.realProduct_pos line 46
5. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.log_realProduct line 50
6. def OAI.Ostmann.Arithmetic.HistoryProductWindows.halfProduct line 55
7. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.halfProduct_log_bound line 58
8. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.compensation_log_bound line 77
9. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.realProduct_eq_product_realEval line 87