OAI/Combinatorics/Progressions/FixedDensity/OrderedPatternPartition.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.OrderedPartitionComplex.topLayer line 14
  2. def OAI.Erdos3.FixedDensity.OrderedPartitionComplex.dropTop line 21
  3. def OAI.Erdos3.FixedDensity.OrderedPartitionComplex.appendTop line 28
  4. def OAI.Erdos3.FixedDensity.OrderedPartitionComplex.withTopLayer line 37
  5. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.topLayer_appendTop line 47
  6. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.dropTop_appendTop line 56
  7. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.topLayer_withTopLayer line 67
  8. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.withTopLayer_partition_castSucc line 76
  9. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.appendTop_partition_castSucc line 87
  10. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.appendTop_partition_last line 98
  11. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.withTopLayer_partition_castSucc_general line 108
  12. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.appendTop_dropTop_topLayer line 119
  13. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.dropTop_refines line 133
  14. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.appendTop_refines line 142
  15. theorem OAI.Erdos3.FixedDensity.OrderedPartitionComplex.withTopLayer_refines line 165
  16. structure OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex line 185
  17. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.boundaryRefines line 194
  18. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceAtomEnergyGap line 203
  19. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceAtomEnergyGap_nonneg line 215
  20. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.layerAtomEnergyGap line 226
  21. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.layerAtomEnergyGap_eq_sum_face line 238
  22. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.layerAtomEnergyGap_nonneg line 251
  23. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.layerAtomEnergyGap_le_card line 262
  24. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.totalAtomEnergyGap line 288
  25. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.totalAtomEnergyGap_nonneg line 294
  26. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceAtomEnergyGap_le_layer line 302
  27. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.layerAtomEnergyGap_le_total line 314
  28. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceAtomEnergyGap_le_total line 326
  29. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.totalAtomEnergyGap_le line 336
  30. abbrev OAI.Erdos3.FixedDensity.OrderedRegularityTolerance line 348
  31. abbrev OAI.Erdos3.FixedDensity.OrderedRegularityBudget line 350
  32. abbrev OAI.Erdos3.FixedDensity.OrderedRegularityStepSchedule line 352
  33. def OAI.Erdos3.FixedDensity.IsFullyPreliminaryOrderedRegular line 354
  34. def OAI.Erdos3.FixedDensity.IsOrderedRegularityBudget line 365
  35. def OAI.Erdos3.FixedDensity.HasOrderedRegularityComplexityBound line 373
  36. structure OAI.Erdos3.FixedDensity.FullOrderedRegularityCertificate line 385
  37. theorem OAI.Erdos3.FixedDensity.exists_fullOrderedRegularityCertificate line 403
  38. theorem OAI.Erdos3.FixedDensity.exists_fullyPreliminaryOrderedRegular_refinement line 590
  39. def OAI.Erdos3.FixedDensity.OrderedPattern.edgeFinset line 622
  40. theorem OAI.Erdos3.FixedDensity.OrderedPattern.mem_edgeFinset line 630
  41. def OAI.Erdos3.FixedDensity.orderedPatternTopPartition line 637
  42. theorem OAI.Erdos3.FixedDensity.complexity_orderedPatternTopPartition_le_two line 646
  43. theorem OAI.Erdos3.FixedDensity.mem_of_mem_part_of_le_generatedBy_singleton line 657
  44. theorem OAI.Erdos3.FixedDensity.orderedPattern_edge_of_mem_refinedTopAtom line 674
  45. def OAI.Erdos3.FixedDensity.indiscreteOrderedPartitionComplex line 689
  46. def OAI.Erdos3.FixedDensity.orderedPatternInitialComplex line 694
  47. theorem OAI.Erdos3.FixedDensity.orderedPatternInitialComplex_topLayer line 702
  48. theorem OAI.Erdos3.FixedDensity.orderedPatternTopPartition_refines_of_complex_refines_initial line 709
  49. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.edge_of_mem_topAtom line 723
  50. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.isOccurrence_of_mem_topAtoms line 750