OAI/Combinatorics/Honeycomb/FiniteCylinder.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

Finite hard-core cylinder partitions and planar polygon bounds.

  1. abbrev OAI.HoneycombCylinder.FiniteHardCore.Independent line 18
  2. def OAI.HoneycombCylinder.FiniteHardCore.partition line 21
  3. def OAI.HoneycombCylinder.FiniteHardCore.neighbors line 26
  4. lemma OAI.HoneycombCylinder.FiniteHardCore.independent_insert line 30
  5. lemma OAI.HoneycombCylinder.FiniteHardCore.partition_insert line 42
  6. lemma OAI.HoneycombCylinder.FiniteHardCore.partition_empty line 81
  7. lemma OAI.HoneycombCylinder.FiniteHardCore.coeff_zero line 85
  8. lemma OAI.HoneycombCylinder.FiniteHardCore.coeff_one line 97
  9. def OAI.HoneycombCylinder.FiniteHardCore.compatiblePairs line 108
  10. lemma OAI.HoneycombCylinder.FiniteHardCore.compatiblePairs_insert line 112
  11. lemma OAI.HoneycombCylinder.FiniteHardCore.twice_coeff_two line 139
  12. def OAI.HoneycombCylinder.FiniteHardCore.incompatiblePairs line 151
  13. lemma OAI.HoneycombCylinder.FiniteHardCore.pair_decomposition line 155
  14. lemma OAI.HoneycombCylinder.FiniteHardCore.negative_log_second_derivative line 172
  15. theorem OAI.HoneycombCylinder.FiniteHardCore.log_second_derivative_eq_incompatiblePairs line 188
  16. lemma OAI.HoneycombCylinder.FiniteHardCore.eval_partition line 197
  17. abbrev OAI.HoneycombCylinder.Lattice.Face line 220
  18. abbrev OAI.HoneycombCylinder.Lattice.Vertex line 221
  19. abbrev OAI.HoneycombCylinder.Lattice.Bond line 222
  20. def OAI.HoneycombCylinder.Lattice.bondSource line 226
  21. def OAI.HoneycombCylinder.Lattice.bondTarget line 228
  22. def OAI.HoneycombCylinder.Lattice.dualEnds line 233
  23. def OAI.HoneycombCylinder.Lattice.vertices line 238
  24. def OAI.HoneycombCylinder.Lattice.Incident line 241
  25. def OAI.HoneycombCylinder.Lattice.AdjWithin line 244
  26. def OAI.HoneycombCylinder.Lattice.IsCycle line 248
  27. abbrev OAI.HoneycombCylinder.Lattice.Polygon line 254
  28. def OAI.HoneycombCylinder.Lattice.Polygon.vertices line 259
  29. def OAI.HoneycombCylinder.Lattice.Polygon.length line 261
  30. def OAI.HoneycombCylinder.Lattice.Polygon.Incompatible line 263
  31. lemma OAI.HoneycombCylinder.Lattice.Polygon.vertices_nonempty line 266
  32. lemma OAI.HoneycombCylinder.Lattice.Polygon.incompatible_symm line 271
  33. lemma OAI.HoneycombCylinder.Lattice.Polygon.incompatible_self line 276
  34. lemma OAI.HoneycombCylinder.Lattice.Polygon.not_incompatible_iff_disjoint line 280
  35. def OAI.HoneycombCylinder.Lattice.DualAvoiding line 286
  36. def OAI.HoneycombCylinder.Lattice.Separates line 291
  37. def OAI.HoneycombCylinder.Lattice.InHex line 294
  38. def OAI.HoneycombCylinder.Lattice.TriangleInHex line 297
  39. def OAI.HoneycombCylinder.Lattice.ContainedInHex line 301
  40. def OAI.HoneycombCylinder.Lattice.SurroundsOrigin line 304
  41. def OAI.HoneycombCylinder.criticalActivity line 312
  42. abbrev OAI.HoneycombCylinder.CylFace line 314
  43. abbrev OAI.HoneycombCylinder.CylPolygon line 315
  44. def OAI.HoneycombCylinder.firstMark line 317
  45. def OAI.HoneycombCylinder.secondMark line 318
  46. abbrev OAI.HoneycombCylinder.SeparatingPolygon line 320
  47. def OAI.HoneycombCylinder.cylinderLength line 323
  48. def OAI.HoneycombCylinder.CylinderIncompatible line 325
  49. abbrev OAI.HoneycombCylinder.CylinderConfiguration line 328
  50. def OAI.HoneycombCylinder.cylinderWeight line 332
  51. def OAI.HoneycombCylinder.cylinderComplexWeight line 335
  52. def OAI.HoneycombCylinder.G line 338
  53. def OAI.HoneycombCylinder.GComplex line 340
  54. def OAI.HoneycombCylinder.pairWeight line 342
  55. def OAI.HoneycombCylinder.pairMass line 346
  56. def OAI.HoneycombCylinder.cylinderFluctuation line 348
  57. abbrev OAI.HoneycombCylinder.PlanarPolygon line 351
  58. def OAI.HoneycombCylinder.PlanarIncompatible line 354
  59. abbrev OAI.HoneycombCylinder.PlanarConfiguration line 357
  60. def OAI.HoneycombCylinder.planarWeight line 361
  61. def OAI.HoneycombCylinder.Z line 364
  62. def OAI.HoneycombCylinder.evenAtTop line 366
  63. def OAI.HoneycombCylinder.stripExponent line 368
  64. lemma OAI.HoneycombCylinder.criticalActivity_pos line 371
  65. def OAI.HoneycombCylinder.cutBond line 376
  66. lemma OAI.HoneycombCylinder.cutBond_dualEnds line 378
  67. lemma OAI.HoneycombCylinder.separator_meets_cut line 382
  68. def OAI.HoneycombCylinder.cutIndex line 399
  69. lemma OAI.HoneycombCylinder.cutIndex_spec line 402
  70. lemma OAI.HoneycombCylinder.source_mem_vertices line 406
  71. lemma OAI.HoneycombCylinder.cylinder_configuration_card_le line 411
  72. lemma OAI.HoneycombCylinder.cylinder_configuration_card_le_two_mul line 426
  73. def OAI.HoneycombCylinder.emptyCylinderConfiguration line 431
  74. lemma OAI.HoneycombCylinder.cylinderWeight_empty line 434
  75. lemma OAI.HoneycombCylinder.cylinderComplexWeight_empty line 438
  76. lemma OAI.HoneycombCylinder.cylinderWeight_zero_of_ne_empty line 442
  77. lemma OAI.HoneycombCylinder.cylinderComplexWeight_zero_of_ne_empty line 448
  78. theorem OAI.HoneycombCylinder.G_zero line 454
  79. theorem OAI.HoneycombCylinder.GComplex_zero line 459
  80. def OAI.HoneycombCylinder.cylinderCutoff line 474
  81. lemma OAI.HoneycombCylinder.mem_cylinderCutoff line 479
  82. def OAI.HoneycombCylinder.heightBonds line 483
  83. def OAI.HoneycombCylinder.finiteCylinderPolynomial line 488
  84. lemma OAI.HoneycombCylinder.finiteCylinderPolynomial_eval line 492
  85. lemma OAI.HoneycombCylinder.finiteCylinderPolynomial_coeff_zero line 503
  86. lemma OAI.HoneycombCylinder.finiteCylinderPolynomial_degree_le line 508
  87. theorem OAI.HoneycombCylinder.finite_cylinder_negative_log_second_derivative line 519
  88. def OAI.HoneycombCylinder.planarBondBox line 532
  89. lemma OAI.HoneycombCylinder.planarPolygon_bonds_subset line 536
  90. def OAI.HoneycombCylinder.planarPolygonCode line 549
  91. instance OAI.HoneycombCylinder.planarPolygon_finite line 557
  92. theorem OAI.HoneycombCylinder.planarWeight_summable line 560
  93. lemma OAI.HoneycombCylinder.planarWeight_nonneg line 563
  94. def OAI.HoneycombCylinder.emptyPlanarConfiguration line 569
  95. lemma OAI.HoneycombCylinder.planarWeight_empty line 571
  96. theorem OAI.HoneycombCylinder.one_le_Z line 575
  97. instance OAI.HoneycombCylinder.evenAtTop_neBot line 580
  98. lemma OAI.HoneycombCylinder.inHex_mono line 595
  99. lemma OAI.HoneycombCylinder.triangleInHex_mono line 600
  100. def OAI.HoneycombCylinder.planarPolygonInclusion line 606
  101. def OAI.HoneycombCylinder.planarConfigurationInclusion line 613
  102. lemma OAI.HoneycombCylinder.planarWeight_inclusion line 625
  103. theorem OAI.HoneycombCylinder.Z_mono line 632