OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkCorrectedXiBoundsRemoved.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

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

   Also declared: OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkCorrectedXiBoundsBasic.lean:15 (same declaration text).

2. theorem OAI.Ostmann.Arithmetic.HistoryBulkCorrectedXiBounds.actual_history_U_window line 19
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkCorrectedXiBounds.selected_paired_U_window line 63