OAI/Combinatorics/Progressions/Geometry/QuantitativeMetricPartition.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.metric_cover_of_box_grid line 17
2. def OAI.Erdos3.boxCoverMeshCount line 29
3. theorem OAI.Erdos3.boxCoverMeshCount_pos line 32
4. theorem OAI.Erdos3.boxCoverMeshCount_error line 36
5. theorem OAI.Erdos3.exists_finite_metric_cover_of_box line 45
6. def OAI.Erdos3.metricTent line 67
7. theorem OAI.Erdos3.metricTent_nonneg line 69
8. theorem OAI.Erdos3.metricTent_le line 71
9. theorem OAI.Erdos3.metricTent_zero_of_far line 74
10. theorem OAI.Erdos3.abs_metricTent_sub_le line 77
11. theorem OAI.Erdos3.lipschitz_metricTent line 87
12. def OAI.Erdos3.metricTentSum line 94
13. theorem OAI.Erdos3.metricTentSum_ge line 96
14. theorem OAI.Erdos3.abs_metricTentSum_sub_le line 103
15. def OAI.Erdos3.metricTentPartition line 112
16. theorem OAI.Erdos3.metricTentPartition_nonneg line 115
17. theorem OAI.Erdos3.sum_metricTentPartition line 119
18. theorem OAI.Erdos3.metricTentPartition_le_one line 124
19. theorem OAI.Erdos3.metricTentPartition_zero_of_far line 129
20. theorem OAI.Erdos3.abs_metricTentPartition_sub_le line 133
21. theorem OAI.Erdos3.lipschitz_metricTentPartition line 146
22. theorem OAI.Erdos3.boxCoverMeshCount_add_one_le_exp line 164
23. theorem OAI.Erdos3.boxCoverCount_le_exp line 184
24. theorem OAI.Erdos3.exists_metric_partition_of_box line 224
25. theorem OAI.Erdos3.shifted_power_self_mono line 264
26. theorem OAI.Erdos3.metricPartition_constant_le_exp line 270
27. theorem OAI.Erdos3.metricPartition_constant_power_budget line 285
28. theorem OAI.Erdos3.exists_metric_partition_exp_bound line 317