OAI/Combinatorics/StripMass/LocalPadding.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.Position.padTop line 17
  2. def OAI.CriticalStrip.Diagram.Position.padBottom line 19
  3. lemma OAI.CriticalStrip.Diagram.Pairing.map_injective line 24
  4. lemma OAI.CriticalStrip.Diagram.optionMatrix_map line 29
  5. lemma OAI.CriticalStrip.Diagram.localR_padTop line 36
  6. lemma OAI.CriticalStrip.Diagram.localR_padBottom line 47
  7. lemma OAI.CriticalStrip.Diagram.localR_zero_of_support line 58
  8. lemma OAI.CriticalStrip.Diagram.localR_padTop_outside line 71
  9. lemma OAI.CriticalStrip.Diagram.localR_padBottom_outside line 81
  10. lemma OAI.CriticalStrip.Diagram.localR_top_matrix line 91
  11. lemma OAI.CriticalStrip.Diagram.localR_bottom_matrix line 103
  12. lemma OAI.CriticalStrip.Diagram.PartialColumn.program_congr line 126
  13. lemma OAI.CriticalStrip.Diagram.PartialColumn.program_commute line 135
  14. lemma OAI.CriticalStrip.Diagram.PartialColumn.exchange_program line 147
  15. lemma OAI.CriticalStrip.Diagram.TriplePosition.coefficient_replacement line 191
  16. theorem OAI.CriticalStrip.Diagram.TriplePosition.deletion line 219
  17. theorem OAI.CriticalStrip.Diagram.TriplePosition.merge line 234
  18. lemma OAI.CriticalStrip.Diagram.PartialColumn.program_zero_above line 259
  19. lemma OAI.CriticalStrip.Diagram.PartialColumn.exchange_program_column line 278
  20. def OAI.CriticalStrip.Diagram.PartialColumn.rowPosition line 340
  21. def OAI.CriticalStrip.Diagram.PartialColumn.rowTriple line 343
  22. lemma OAI.CriticalStrip.Diagram.PartialColumn.row_disjoint_low line 346
  23. lemma OAI.CriticalStrip.Diagram.PartialColumn.row_disjoint_high line 352
  24. theorem OAI.CriticalStrip.Diagram.PartialColumn.torus_column_exchange line 359
  25. lemma OAI.CriticalStrip.Diagram.PartialColumn.column_restricted_train line 405
  26. theorem OAI.CriticalStrip.Diagram.PartialColumn.column_deletion line 432
  27. theorem OAI.CriticalStrip.Diagram.PartialColumn.column_merge line 463
  28. def OAI.CriticalStrip.Diagram.functionMatrix line 502
  29. lemma OAI.CriticalStrip.Diagram.functionMatrix_mul line 504
  30. lemma OAI.CriticalStrip.Diagram.mul_functionMatrix line 508
  31. lemma OAI.CriticalStrip.Diagram.functionMatrix_mul_apply line 516
  32. lemma OAI.CriticalStrip.Diagram.functionMatrix_mul_outside line 526
  33. lemma OAI.CriticalStrip.Diagram.optionMatrix_natural line 534
  34. lemma OAI.CriticalStrip.Diagram.localR_natural line 549
  35. lemma OAI.Fin.swap_succAbove_adjacent line 570