OAI/Combinatorics/Progressions/FixedDensity/OrderedBoundaryPartition.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.FixedDensity.eraseOrderedFace line 11
2. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_eraseOrderedFace line 20
3. theorem OAI.Erdos3.FixedDensity.exists_orderedCoface line 31
4. def OAI.Erdos3.FixedDensity.OrderedPattern.deletionCylinder line 114
5. theorem OAI.Erdos3.FixedDensity.OrderedPattern.mem_deletionCylinder line 125
6. theorem OAI.Erdos3.FixedDensity.OrderedPattern.card_deletionCylinder line 136
7. def OAI.Erdos3.FixedDensity.OrderedPattern.liftLowerDeletion line 170
8. theorem OAI.Erdos3.FixedDensity.OrderedPattern.mem_liftLowerDeletion line 181
9. theorem OAI.Erdos3.FixedDensity.OrderedPattern.card_liftLowerDeletion_le line 193
10. theorem OAI.Erdos3.FixedDensity.OrderedPattern.deletionCylinder_density_eq line 204
11. theorem OAI.Erdos3.FixedDensity.OrderedPattern.faceDeletionDensity_liftLowerDeletion_le line 228
12. def OAI.Erdos3.FixedDensity.OrderedPattern.unionDeletion line 270
13. theorem OAI.Erdos3.FixedDensity.OrderedPattern.mem_unionDeletion line 281
14. theorem OAI.Erdos3.FixedDensity.OrderedPattern.faceDeletionDensity_unionDeletion_le line 292
15. theorem OAI.Erdos3.FixedDensity.OrderedPattern.toWeighted_edgeWeight_zeroOne line 321
16. def OAI.Erdos3.FixedDensity.OrderedPattern.lowStructuredDeletion line 334
17. theorem OAI.Erdos3.FixedDensity.OrderedPattern.mem_lowStructuredDeletion line 346
18. theorem OAI.Erdos3.FixedDensity.OrderedPattern.faceDeletionDensity_lowStructuredDeletion_le line 361
19. theorem OAI.Erdos3.FixedDensity.OrderedPattern.regularized_edgeWeight_ge_of_not_mem_lowDeletion line 376
20. theorem OAI.Erdos3.FixedDensity.OrderedPattern.lowerCover_lifts line 400
21. def OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.IsInAtomBranch line 427
22. def OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.lowerCellPattern line 442
23. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.lowerCellPattern_isOccurrence_iff line 458
24. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.mem_all_topAtoms_iff_exists_branchSystem line 478
25. def OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.atomEdgeWeight line 516
26. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.regularized_edgeWeight_eq_atomEdgeWeight line 527
27. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.regularized_patternWeight_eq_prod_atomEdgeWeight line 545
28. def OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.IsHeavy line 562
29. abbrev OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.CellIndex line 571
30. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.card_cellIndex line 580
31. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.card_cellIndex_le line 591
32. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.pow_le_regularized_patternWeight_of_lowerCellOccurrence line 608
33. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.pow_mul_lowerCellPattern_weight_le line 641
34. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.pow_mul_lowerCellPattern_count_le line 670
35. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.lowerCellPattern_count_lt_of_regularized_count_lt line 690
36. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.exists_generatedCellCover_of_activeLowerCellCounts line 717
37. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.exists_generatedCellCover_of_lowerCellCounts line 984
38. theorem OAI.Erdos3.FixedDensity.GeneratedOrderedPatternRegularization.exists_generatedCellCover line 1030
39. def OAI.Erdos3.FixedDensity.eraseBoundaryCoordinate line 1081
40. def OAI.Erdos3.FixedDensity.eraseBoundaryFace line 1087
41. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_eraseBoundaryFace line 1094
42. abbrev OAI.Erdos3.FixedDensity.OrderedFacePartitionSystem line 1102
43. def OAI.Erdos3.FixedDensity.OrderedFacePartitionRefines line 1107
44. theorem OAI.Erdos3.FixedDensity.OrderedFacePartitionRefines.refl line 1115
45. theorem OAI.Erdos3.FixedDensity.OrderedFacePartitionRefines.trans line 1122
46. def OAI.Erdos3.FixedDensity.indiscreteOrderedFacePartitionSystem line 1133
47. def OAI.Erdos3.FixedDensity.orderedImmediateBoundaryPartition line 1139
48. def OAI.Erdos3.FixedDensity.orderedBoundaryPartition line 1148
49. theorem OAI.Erdos3.FixedDensity.orderedBoundaryPartition_le_immediate line 1158
50. theorem OAI.Erdos3.FixedDensity.orderedBoundaryPartition_mono line 1169
51. theorem OAI.Erdos3.FixedDensity.mem_orderedBoundaryPartition_part_iff line 1185
52. theorem OAI.Erdos3.FixedDensity.mem_orderedBoundaryPartition_part_iff_part_eq line 1202
53. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_mem_boundary_part_iff line 1229
54. theorem OAI.Erdos3.FixedDensity.complexity_orderedBoundaryPartition_le line 1253
55. theorem OAI.Erdos3.FixedDensity.complexity_orderedBoundaryPartition_le_pow line 1283
56. def OAI.Erdos3.FixedDensity.orderedBoundaryAtomAt line 1307
57. theorem OAI.Erdos3.FixedDensity.orderedBoundaryAtomAt_val line 1319
58. theorem OAI.Erdos3.FixedDensity.mem_orderedBoundaryAtomAt_iff line 1329
59. def OAI.Erdos3.FixedDensity.orderedBoundaryStructured line 1342
60. def OAI.Erdos3.FixedDensity.orderedBoundaryEnergy line 1351
61. theorem OAI.Erdos3.FixedDensity.orderedBoundaryEnergy_mono line 1359
62. theorem OAI.Erdos3.FixedDensity.orderedBoundaryEnergy_sub_eq_mean_sq line 1373
63. structure OAI.Erdos3.FixedDensity.OrderedPartitionComplex line 1390
64. def OAI.Erdos3.FixedDensity.OrderedPartitionComplex.layer line 1400
65. def OAI.Erdos3.FixedDensity.OrderedPartitionComplex.boundary line 1408
66. def OAI.Erdos3.FixedDensity.OrderedPartitionComplex.Refines line 1417
67. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.Refines.refl line 1423
68. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.Refines.trans line 1430
69. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.boundary_mono line 1438