OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/FixedBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryRationalWidth.fixedBudget line 27
2. lemma OAI.OrdinaryRationalWidth.rational_fixed_limit line 31
3. lemma OAI.OrdinaryRationalWidth.bin_card_le line 44
4. lemma OAI.OrdinaryRationalWidth.fixed_budget_le line 49
5. lemma OAI.OrdinaryRationalWidth.sqrt_subadd line 98
6. theorem OAI.OrdinaryRationalWidth.grid_fixed_budget_bound line 105
7. def OAI.OrdinaryRationalWidth.packetBudget line 138
8. def OAI.OrdinaryRationalWidth.packetFixed line 143
9. lemma OAI.OrdinaryRationalWidth.packet_limit line 149
10. theorem OAI.OrdinaryRationalWidth.minor_arc_explicit_width line 160