OAI/Combinatorics/Progressions/FixedDensity/StructuredCleaning.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.FixedDensity.IsZeroOneValued line 12
2. def OAI.Erdos3.FixedDensity.FaceRegularityState.structuredSublevel line 17
3. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.mem_structuredSublevel line 25
4. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.structuredSublevel_measurable line 33
5. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.mean_mul_structuredSublevel_eq line 62
6. def OAI.Erdos3.FixedDensity.FaceRegularityState.lowStructuredOneFinset line 75
7. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.mem_lowStructuredOneFinset line 84
8. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.indicator_lowStructuredOneFinset line 92
9. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.mean_indicator_lowStructuredOneFinset_le line 119
10. def OAI.Erdos3.FixedDensity.deletedFaceEquiv line 152
11. theorem OAI.Erdos3.FixedDensity.canonicalEdgeFunction_toWeighted_zeroOne line 161
12. def OAI.Erdos3.FixedDensity.lowStructuredDeletion line 177
13. theorem OAI.Erdos3.FixedDensity.card_lowStructuredDeletion line 190
14. theorem OAI.Erdos3.FixedDensity.mem_lowStructuredDeletion_iff line 203
15. theorem OAI.Erdos3.FixedDensity.lowStructuredDeletion_isEdgeDeletion line 234
16. theorem OAI.Erdos3.FixedDensity.colorDeletionDensity_lowStructuredDeletion_le line 260
17. theorem OAI.Erdos3.FixedDensity.normalizedDeletionCost_lowStructuredDeletion_le line 285
18. theorem OAI.Erdos3.FixedDensity.regularized_edgeWeight_ge_of_not_mem_lowDeletion line 346
19. theorem OAI.Erdos3.FixedDensity.pow_le_regularized_simplexWeight_of_avoids_lowDeletion line 385
20. theorem OAI.Erdos3.FixedDensity.lowStructuredDeletion_isSimplexCover_of_count_lt line 418