OAI/Combinatorics/Honeycomb/PolygonMoment.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Honeycomb.Cell line 11
  2. structure OAI.Honeycomb.Vertex line 13
  3. structure OAI.Honeycomb.Edge line 21
  4. def OAI.Honeycomb.Edge.p line 27
  5. def OAI.Honeycomb.Edge.r line 29
  6. def OAI.Honeycomb.Edge.ends line 33
  7. def OAI.Honeycomb.h line 35
  8. def OAI.Honeycomb.v line 36
  9. def OAI.Honeycomb.cellPosition line 38
  10. def OAI.Honeycomb.position line 41
  11. def OAI.Honeycomb.cyclicSucc line 44
  12. def OAI.Honeycomb.IsSimpleCycle line 49
  13. structure OAI.Honeycomb.EmbeddedPolygon line 53
  14. theorem OAI.Honeycomb.EmbeddedPolygon.ext line 57
  15. theorem OAI.Honeycomb.EmbeddedPolygon.edges_nonempty line 64
  16. def OAI.Honeycomb.Vertex.translate line 72
  17. def OAI.Honeycomb.Edge.translate line 75
  18. theorem OAI.Honeycomb.Edge.translate_zero line 78
  19. theorem OAI.Honeycomb.Edge.translate_translate line 82
  20. theorem OAI.Honeycomb.Edge.translate_injective line 87
  21. theorem OAI.Honeycomb.Edge.p_translate line 92
  22. theorem OAI.Honeycomb.Edge.r_translate line 95
  23. theorem OAI.Honeycomb.position_translate line 100
  24. def OAI.Honeycomb.translateEdges line 105
  25. theorem OAI.Honeycomb.translateEdges_zero line 108
  26. theorem OAI.Honeycomb.translateEdges_translate line 112
  27. theorem OAI.Honeycomb.translateEdges_card line 119
  28. def OAI.Honeycomb.vertices line 124
  29. def OAI.Honeycomb.pointSet line 126
  30. def OAI.Honeycomb.embeddedDiameter line 128
  31. theorem OAI.Honeycomb.vertices_translate line 130
  32. theorem OAI.Honeycomb.pointSet_translate line 134
  33. theorem OAI.Honeycomb.embeddedDiameter_translate line 139
  34. def OAI.Honeycomb.TranslationEquivalent line 146
  35. instance OAI.Honeycomb.polygonSetoid line 149
  36. abbrev OAI.Honeycomb.Polygon line 168
  37. def OAI.Honeycomb.length line 170
  38. def OAI.Honeycomb.diameter line 175
  39. def OAI.Honeycomb.xStar line 181
  40. def OAI.Honeycomb.weight line 183
  41. def OAI.Honeycomb.massTerm line 185
  42. def OAI.Honeycomb.lengthTerm line 188
  43. def OAI.Honeycomb.secondMomentTerm line 191
  44. def OAI.Honeycomb.A line 195
  45. def OAI.Honeycomb.P line 198
  46. def OAI.Honeycomb.M2 line 201
  47. theorem OAI.Honeycomb.Edge.ends_injective line 205
  48. theorem OAI.Honeycomb.diameter_nonneg line 224
  49. theorem OAI.Honeycomb.xStar_pos line 228
  50. theorem OAI.Honeycomb.xStar_lt_one line 232
  51. theorem OAI.Honeycomb.weight_pos line 239
  52. theorem OAI.Honeycomb.weight_nonneg line 241
  53. theorem OAI.Honeycomb.massTerm_nonneg line 243
  54. theorem OAI.Honeycomb.lengthTerm_nonneg line 248
  55. theorem OAI.Honeycomb.secondMomentTerm_nonneg line 253
  56. theorem OAI.Honeycomb.A_nonneg line 258
  57. theorem OAI.Honeycomb.P_nonneg line 259
  58. theorem OAI.Honeycomb.M2_nonneg line 260
  59. def OAI.Honeycomb.anchor line 264
  60. theorem OAI.Honeycomb.anchor_mem line 266
  61. def OAI.Honeycomb.anchorCell line 269
  62. def OAI.Honeycomb.anchoredEdges line 271
  63. theorem OAI.Honeycomb.anchoredEdges_injective line 274
  64. theorem OAI.Honeycomb.embeddedDiameter_out line 283
  65. theorem OAI.Honeycomb.anchoredEdges_diameter line 288
  66. theorem OAI.Honeycomb.pointSet_finite line 292
  67. theorem OAI.Honeycomb.p_mem_pointSet line 295
  68. theorem OAI.Honeycomb.zero_mem_anchored_pointSet line 299
  69. theorem OAI.Honeycomb.norm_position_p_le_diameter line 306
  70. theorem OAI.Honeycomb.position_p_re line 315
  71. theorem OAI.Honeycomb.position_p_im line 319
  72. theorem OAI.Honeycomb.edge_coordinate_bound line 324
  73. def OAI.Honeycomb.edgeBox line 362
  74. theorem OAI.Honeycomb.mem_edgeBox line 366
  75. theorem OAI.Honeycomb.anchoredEdges_subset_box line 377
  76. theorem OAI.Honeycomb.finite_diameter_le line 393
  77. theorem OAI.Honeycomb.summable_diameter_truncation line 401
  78. theorem OAI.Honeycomb.summable_secondMomentTerm line 409
  79. theorem OAI.Honeycomb.M2_monotone line 413
  80. instance OAI.Honeycomb.(instance at line 427) line 427
  81. instance OAI.Honeycomb.(instance at line 433) line 433
  82. theorem OAI.Honeycomb.polygon_countable line 439
  83. theorem OAI.Honeycomb.length_pos line 441
  84. def OAI.Honeycomb.hexagonEdges line 445
  85. def OAI.Honeycomb.hexagon line 449
  86. theorem OAI.Honeycomb.hexagon_length line 457
  87. instance OAI.Honeycomb.(instance at line 459) line 459
  88. theorem OAI.Honeycomb.Edge.unit_length line 462
  89. theorem OAI.Honeycomb.position_injective line 473