OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkCorrectedXiBoundsBasic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkCorrectedXiBounds.sum_filter_map line 15

   Also declared: OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkCorrectedXiBoundsRemoved.lean:13 (same declaration text).

2. theorem OAI.Ostmann.Arithmetic.HistoryBulkCorrectedXiBounds.log_role_product line 21
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkCorrectedXiBounds.remaining_log_error line 34
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkCorrectedXiBounds.actual_history_H_window line 73