OAI/Combinatorics/HoneycombBridges/Basic.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Strict honeycomb bridges and their finite length classes.

  1. structure OAI.HoneycombActual.Vertex line 15
  2. def OAI.HoneycombActual.up line 21
  3. def OAI.HoneycombActual.down line 22
  4. def OAI.HoneycombActual.UpDownAdj line 24
  5. def OAI.HoneycombActual.Adj line 30
  6. def OAI.HoneycombActual.rowSpacing line 32
  7. def OAI.HoneycombActual.position line 34
  8. def OAI.HoneycombActual.port line 42
  9. structure OAI.HoneycombActual.Bridge line 45
  10. def OAI.HoneycombActual.Bridge.length line 58
  11. def OAI.HoneycombActual.Bridge.endpointDistance line 60
  12. def OAI.HoneycombActual.Bridge.trace line 63
  13. def OAI.HoneycombActual.Bridge.diameter line 66
  14. def OAI.HoneycombActual.Bridge.crosses line 68
  15. def OAI.HoneycombActual.Bridge.crossingCount line 72
  16. def OAI.HoneycombActual.Bridge.Irreducible line 75
  17. def OAI.HoneycombActual.rho line 80
  18. def OAI.HoneycombActual.weight line 82
  19. def OAI.HoneycombActual.criticalMass line 84
  20. def OAI.HoneycombActual.bridgeMass line 88
  21. def OAI.HoneycombActual.lengthReward line 91
  22. def OAI.HoneycombActual.uniformLengthProbability line 95
  23. def OAI.HoneycombActual.FiniteBridgeEstimates line 99
  24. def OAI.HoneycombActual.ExactLengthSpatialLaw line 112
  25. theorem OAI.HoneycombActual.rho_pos line 119
  26. theorem OAI.HoneycombActual.Adj.side_ne line 123
  27. theorem OAI.HoneycombActual.chain_length_parity line 126
  28. theorem OAI.HoneycombActual.Bridge.even_length line 144
  29. def OAI.HoneycombActual.zigzagTwo line 158
  30. def OAI.HoneycombActual.zigzagFour line 172
  31. theorem OAI.HoneycombActual.Bridge.irreducible_of_height_one line 186
  32. theorem OAI.HoneycombActual.zigzagTwo_irreducible line 191
  33. theorem OAI.HoneycombActual.zigzagFour_irreducible line 194
  34. theorem OAI.HoneycombActual.weight_pos line 197
  35. theorem OAI.HoneycombActual.weight_le_criticalMass line 200
  36. def OAI.HoneycombActual.halfLengthMass line 209
  37. theorem OAI.HoneycombActual.halfLengthMass_one_pos line 212
  38. theorem OAI.HoneycombActual.halfLengthMass_two_pos line 217
  39. def OAI.HoneycombActual.SpanOne line 222
  40. theorem OAI.HoneycombActual.actual_halfLength_span_one line 226
  41. def OAI.HoneycombActual.neighbors line 236
  42. theorem OAI.HoneycombActual.mem_neighbors_iff line 242
  43. def OAI.HoneycombActual.walkLists line 248
  44. theorem OAI.HoneycombActual.isChain_mem_walkLists line 252
  45. theorem OAI.HoneycombActual.Bridge.vertices_mem_walkLists line 263
  46. theorem OAI.HoneycombActual.Bridge.length_pos line 274
  47. theorem OAI.HoneycombActual.Bridge.vertices_injective line 280
  48. instance OAI.HoneycombActual.finiteBridgeLength line 296
  49. instance OAI.HoneycombActual.finiteBridgeLengthEvent line 306
  50. theorem OAI.HoneycombActual.exactLengthMass_eq line 315
  51. theorem OAI.HoneycombActual.lengthMass_eq line 339
  52. theorem OAI.HoneycombActual.lengthMass_ne_top line 363
  53. theorem OAI.HoneycombActual.uniformLengthProbability_eq_critical_ratio line 367
  54. theorem OAI.HoneycombActual.Bridge.halfLength_pos line 376
  55. theorem OAI.HoneycombActual.Bridge.twice_halfLength line 381
  56. theorem OAI.HoneycombActual.halfLengthMass_eq_pushforward line 385
  57. theorem OAI.HoneycombActual.halfLengthMass_zero line 393
  58. def OAI.HoneycombActual.rowVertex line 407
  59. theorem OAI.HoneycombActual.rowVertex_injective line 410
  60. theorem OAI.HoneycombActual.rowVertex_adj line 417
  61. def OAI.HoneycombActual.rowZigzag line 426
  62. theorem OAI.HoneycombActual.rowZigzag_length line 454
  63. theorem OAI.HoneycombActual.rowZigzag_irreducible line 457
  64. theorem OAI.HoneycombActual.nonempty_bridgeLength line 462
  65. theorem OAI.HoneycombActual.card_bridgeLength_pos line 466
  66. theorem OAI.HoneycombActual.Bridge.trace_finite line 471
  67. theorem OAI.HoneycombActual.Bridge.endpointDistance_le_diameter line 474
  68. def OAI.HoneycombActual.IrreducibleNormalization line 478
  69. def OAI.HoneycombActual.lengthLaplaceReward line 480
  70. def OAI.HoneycombActual.ActualLengthTailBound line 485
  71. def OAI.HoneycombActual.ActualLengthLaplaceLower line 490
  72. def OAI.HoneycombActual.ActualLengthLaplaceUpper line 494