OAI/Combinatorics/Progressions/Estimates/LocalWeightCaps.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.cellAverage_le_shifted line 14
2. theorem OAI.Erdos3.translated_slice_le line 23
3. theorem OAI.Erdos3.translated_slice_nonneg line 28
4. theorem OAI.Erdos3.expect_translated_slice line 33
5. theorem OAI.Erdos3.normalized_local_cell_cap line 40