OAI/Combinatorics/StripMass/HeightOne.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.integerLinePath_unique line 12
  2. def OAI.CriticalStrip.oneBandPath line 46
  3. theorem OAI.CriticalStrip.oneBandPath_spec line 49
  4. theorem OAI.CriticalStrip.oneBandPath_unique line 64
  5. theorem OAI.CriticalStrip.oneBandPath_length line 86
  6. theorem OAI.CriticalStrip.isPath_one_iff line 92
  7. theorem OAI.CriticalStrip.archWeight_one line 98
  8. theorem OAI.CriticalStrip.bridgeWeight_one line 109
  9. theorem OAI.CriticalStrip.hasSum_archWeight_one line 121
  10. theorem OAI.CriticalStrip.hasSum_bridgeWeight_one line 129
  11. theorem OAI.CriticalStrip.K_one line 138
  12. theorem OAI.CriticalStrip.bridgeKernel_one line 141
  13. theorem OAI.CriticalStrip.K_one_right line 144
  14. theorem OAI.CriticalStrip.K_one_left line 151
  15. theorem OAI.CriticalStrip.bridgeKernel_one_right line 155
  16. theorem OAI.CriticalStrip.bridgeKernel_one_left line 161
  17. theorem OAI.CriticalStrip.rho_sq_lt_one line 168
  18. theorem OAI.CriticalStrip.hasSum_K_one line 175
  19. theorem OAI.CriticalStrip.hasSum_bridgeKernel_one line 189
  20. theorem OAI.CriticalStrip.hasSum_moment_one line 200
  21. theorem OAI.CriticalStrip.stripSumsFinite_one line 212
  22. theorem OAI.CriticalStrip.archMass_one line 217
  23. theorem OAI.CriticalStrip.bridgeMass_one line 219
  24. theorem OAI.CriticalStrip.moment_one line 221
  25. theorem OAI.CriticalStrip.two_C_mul_rho line 224
  26. theorem OAI.CriticalStrip.c_eq_sqrt_two_mul_rho line 230
  27. theorem OAI.CriticalStrip.rho_sq line 238
  28. theorem OAI.CriticalStrip.critical_one_band_identity line 244
  29. theorem OAI.CriticalStrip.flux_one line 254
  30. def OAI.CriticalStrip.mirrorTriangle line 265
  31. theorem OAI.CriticalStrip.mirrorTriangle_band line 268
  32. theorem OAI.CriticalStrip.mirrorTriangle_up line 270
  33. theorem OAI.CriticalStrip.mirrorTriangle_down line 274
  34. theorem OAI.CriticalStrip.mirrorTriangle_mirrorTriangle line 278
  35. theorem OAI.CriticalStrip.mirrorTriangle_involutive line 284
  36. theorem OAI.CriticalStrip.mirrorTriangles_involutive line 286
  37. theorem OAI.CriticalStrip.adjacent_mirror_iff line 291
  38. theorem OAI.CriticalStrip.IsPath.mirror line 298
  39. theorem OAI.CriticalStrip.isPath_mirror_iff line 314
  40. theorem OAI.CriticalStrip.archWeight_mirror line 319
  41. theorem OAI.CriticalStrip.bridgeWeight_mirror line 325
  42. theorem OAI.CriticalStrip.K_reflection line 340
  43. theorem OAI.CriticalStrip.bridgeKernel_reflection line 347
  44. theorem OAI.CriticalStrip.hasSum_absoluteMoment line 356
  45. theorem OAI.CriticalStrip.absoluteMoment_eq line 373
  46. theorem OAI.CriticalStrip.summable_K_of_moment line 379
  47. theorem OAI.CriticalStrip.archMass_eq_twice_right line 393
  48. def OAI.CriticalStrip.columnVertex line 409
  49. theorem OAI.CriticalStrip.columnVertex_band line 412
  50. theorem OAI.CriticalStrip.columnVertex_injective line 416