OAI/Combinatorics/StripMass/ReversedConvergence.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.L_reflection line 14
  2. lemma OAI.CriticalStrip.Diagram.physicalWeights_reflection line 20
  3. lemma OAI.CriticalStrip.Diagram.physicalWeights_lambda line 31
  4. lemma OAI.CriticalStrip.Diagram.physicalWeights_lambda_nonneg line 36
  5. lemma OAI.CriticalStrip.Diagram.physicalWeights_reverse_pos line 41
  6. lemma OAI.CriticalStrip.Diagram.physicalWeights_reverse_tile_nonneg line 47
  7. def OAI.CriticalStrip.Diagram.augmentedReversedWeights line 56
  8. def OAI.CriticalStrip.Diagram.reverseDeformationAngles line 59
  9. def OAI.CriticalStrip.Diagram.reverseDeformationWeights line 62
  10. lemma OAI.CriticalStrip.Diagram.reverseDeformationWeights_eq line 65
  11. lemma OAI.CriticalStrip.Diagram.reverseDeformationWeights_physical line 81
  12. lemma OAI.CriticalStrip.Diagram.reverseDeformationWeights_flat line 90
  13. lemma OAI.CriticalStrip.Diagram.augmentedReversed_tile_nonneg line 93
  14. lemma OAI.CriticalStrip.Diagram.reverseDeformationWeights_nonnegative line 99
  15. lemma OAI.CriticalStrip.Diagram.physicalWeights_lambda_pos line 108
  16. lemma OAI.CriticalStrip.Diagram.reverseDeformationWeights_accessible line 112
  17. lemma OAI.CriticalStrip.Diagram.reverseDeformationAngles_scalar_ne_zero line 143
  18. lemma OAI.CriticalStrip.Diagram.reverseDeformationAngles_L_ne_zero line 158
  19. lemma OAI.CriticalStrip.Diagram.reverseDeformationWeights_stationary line 169
  20. lemma OAI.CriticalStrip.Diagram.continuousOn_reverseDeformationWeights_tile line 177
  21. lemma OAI.CriticalStrip.Diagram.continuousOn_reverseDeformationColumn line 193
  22. lemma OAI.CriticalStrip.Diagram.continuous_reverseDeformationAngles line 202
  23. lemma OAI.CriticalStrip.Diagram.continuousOn_reverseDeformationVector line 209
  24. lemma OAI.CriticalStrip.Diagram.summablePowers_identity_bottom line 220
  25. theorem OAI.CriticalStrip.Diagram.augmentedReversed_summablePowers line 239
  26. def OAI.CriticalStrip.Diagram.Tile.horizontalPort line 273
  27. def OAI.CriticalStrip.Diagram.Tile.horizontal line 275
  28. lemma OAI.CriticalStrip.Diagram.Tile.horizontal_involutive line 284
  29. lemma OAI.CriticalStrip.Diagram.Tile.horizontal_adj line 286
  30. lemma OAI.CriticalStrip.Diagram.Tile.horizontal_occupied line 291
  31. lemma OAI.CriticalStrip.Diagram.Tile.horizontal_weight line 296
  32. lemma OAI.CriticalStrip.Diagram.Tile.physical_horizontal_weight line 300
  33. lemma OAI.CriticalStrip.Diagram.Tile.physical_horizontal_weight_two line 304
  34. lemma OAI.CriticalStrip.Diagram.Tile.physical_horizontal line 310
  35. def OAI.CriticalStrip.Diagram.Tile.representative line 329
  36. lemma OAI.CriticalStrip.Diagram.Tile.representative_side line 333
  37. lemma OAI.CriticalStrip.Diagram.Tile.representative_occupied line 337
  38. lemma OAI.CriticalStrip.Diagram.Tile.occupied_triangle line 342
  39. lemma OAI.CriticalStrip.Diagram.Tile.reach_representative line 347
  40. lemma OAI.CriticalStrip.Diagram.Tile.reach_middle line 353
  41. lemma OAI.CriticalStrip.Diagram.Tile.adjacent_projects line 358
  42. abbrev OAI.CriticalStrip.HoneycombPort line 364
  43. def OAI.CriticalStrip.portTriangle line 366
  44. def OAI.CriticalStrip.HoneycombAssignment.portWiring line 374
  45. lemma OAI.CriticalStrip.HoneycombAssignment.portWiring_symm line 381
  46. instance OAI.CriticalStrip.HoneycombAssignment.portWiring_symm_instance line 391
  47. lemma OAI.CriticalStrip.HoneycombAssignment.port_used line 394
  48. lemma OAI.CriticalStrip.HoneycombAssignment.port_in_strip line 413
  49. lemma OAI.CriticalStrip.HoneycombAssignment.port_projects_used line 421
  50. lemma OAI.CriticalStrip.HoneycombAssignment.tile_reach line 431
  51. lemma OAI.CriticalStrip.HoneycombAssignment.port_projects_edge line 436
  52. def OAI.CriticalStrip.HoneycombAssignment.representative line 470
  53. lemma OAI.CriticalStrip.HoneycombAssignment.representative_projects line 473
  54. lemma OAI.CriticalStrip.HoneycombAssignment.representative_used line 479
  55. lemma OAI.CriticalStrip.HoneycombAssignment.port_to_representative line 489
  56. lemma OAI.CriticalStrip.HoneycombAssignment.edge_between_representatives line 494
  57. lemma OAI.CriticalStrip.HoneycombAssignment.up_lifts_edge line 500
  58. lemma OAI.CriticalStrip.HoneycombAssignment.lifts_edge line 516
  59. lemma OAI.CriticalStrip.HoneycombAssignment.port_reach_iff line 529
  60. lemma OAI.CriticalStrip.HoneycombAssignment.port_drains_iff line 542