OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/PrimeWindow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryNarrowGrid.primeWindow line 22
2. def OAI.OrdinaryNarrowGrid.primeBin line 25
3. def OAI.OrdinaryNarrowGrid.evenBinLength line 27
4. lemma OAI.OrdinaryNarrowGrid.lower_ge_start line 29
5. lemma OAI.OrdinaryNarrowGrid.prime_window_bins line 35
6. lemma OAI.OrdinaryNarrowGrid.prime_bins_disjoint line 47
7. lemma OAI.OrdinaryNarrowGrid.bin_width line 52
8. theorem OAI.OrdinaryNarrowGrid.even_bin_cutoff line 64
9. lemma OAI.OrdinaryNarrowGrid.even_bin_length_pos line 93