OAI/Combinatorics/Progressions/Estimates/PhysicalSliceCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.PhysicalSubbox line 9
2. theorem OAI.Erdos3.PhysicalSubbox.length_le line 13
3. theorem OAI.Erdos3.PhysicalSubbox.refl line 18
4. def OAI.Erdos3.ResidueSliceLogCostLE line 21
5. theorem OAI.Erdos3.ResidueSliceLogCostLE.mono line 25
6. theorem OAI.Erdos3.residueSliceLogCostLE_of_bounds line 32