OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/WindowSmall.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryChainScales.WindowSmall line 24
2. lemma OAI.OrdinaryChainScales.windowSmall_of_nonpretentious line 28
3. lemma OAI.OrdinaryChainScales.windowSmall_congr_pos line 38
4. lemma OAI.OrdinaryChainScales.windowSmall_zero line 53
5. lemma OAI.OrdinaryChainScales.sharpWindow_add line 63
6. lemma OAI.OrdinaryChainScales.sharpWindow_const_mul line 66
7. lemma OAI.OrdinaryChainScales.sharpWindow_add_l1 line 70
8. lemma OAI.OrdinaryChainScales.windowSmall_add line 81
9. lemma OAI.OrdinaryChainScales.windowSmall_const_mul line 94
10. lemma OAI.OrdinaryChainScales.windowSmall_finsetSum line 116