OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/FrozenWidthError.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinarySharpWindow.frozen_width_error line 23
2. def OAI.OrdinarySharpWindow.bandCut line 59
3. lemma OAI.OrdinarySharpWindow.bandCut_zero line 60
4. lemma OAI.OrdinarySharpWindow.bandCut_end line 61
5. lemma OAI.OrdinarySharpWindow.bandCut_mono line 63
6. lemma OAI.OrdinarySharpWindow.bandCut_lower line 66
7. lemma OAI.OrdinarySharpWindow.bandCut_upper line 67
8. lemma OAI.OrdinarySharpWindow.bandCut_real_upper line 69
9. lemma OAI.OrdinarySharpWindow.bandCut_real_lower line 79
10. lemma OAI.OrdinarySharpWindow.sharpWindow_partition line 91
11. lemma OAI.OrdinarySharpWindow.sharpWindow_partition_l1 line 104
12. lemma OAI.OrdinarySharpWindow.band_card_sum line 115