OAI/Combinatorics/StripMass/LaurentNumerator.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.evalLaurent_monomial_scale line 14
  2. lemma OAI.CriticalStrip.Diagram.evalLaurent_monomial_quot line 20
  3. def OAI.CriticalStrip.Diagram.torusNumeratorL line 27
  4. lemma OAI.CriticalStrip.Diagram.sineL_map_scale line 35
  5. lemma OAI.CriticalStrip.Diagram.sineL_map_quot line 39
  6. lemma OAI.CriticalStrip.Diagram.torusNumeratorL_map line 43
  7. lemma OAI.CriticalStrip.Diagram.sineL_product_box line 59
  8. lemma OAI.CriticalStrip.Diagram.constant_sineL_box line 64
  9. lemma OAI.CriticalStrip.Diagram.torusNumeratorL_box line 70
  10. lemma OAI.CriticalStrip.Diagram.rawLocal_map line 92
  11. def OAI.CriticalStrip.Diagram.LaurentMatrixBox line 103
  12. lemma OAI.CriticalStrip.Diagram.LaurentMatrixBox.one line 106
  13. lemma OAI.CriticalStrip.Diagram.LaurentMatrixBox.mul line 113
  14. lemma OAI.CriticalStrip.Diagram.LaurentMatrixBox.smul line 121
  15. lemma OAI.CriticalStrip.Diagram.rawLocal_box line 127
  16. lemma OAI.CriticalStrip.Diagram.matrixPrefix_box_partial line 139
  17. lemma OAI.CriticalStrip.Diagram.matrixPrefix_box line 154
  18. lemma OAI.CriticalStrip.Diagram.map_monomialL_add_variable line 167
  19. def OAI.CriticalStrip.Diagram.reducedMovingStepL line 177
  20. lemma OAI.CriticalStrip.Diagram.reducedMovingStepL_scalar line 185
  21. lemma OAI.CriticalStrip.Diagram.torusNumeratorL_pair_map line 195
  22. lemma OAI.CriticalStrip.Diagram.matrix_map_ring_smul line 204
  23. lemma OAI.CriticalStrip.Diagram.reducedMovingStepL_map line 210
  24. lemma OAI.CriticalStrip.Diagram.reducedMovingTrainL_map line 231
  25. def OAI.CriticalStrip.Diagram.interpolationNumerator line 247
  26. lemma OAI.CriticalStrip.Diagram.vandermonde_mulVec_coeff line 251
  27. lemma OAI.CriticalStrip.Diagram.interpolationNumerator_eq_det_mul_coeff line 266
  28. lemma OAI.CriticalStrip.Diagram.interpolationNumerator_map line 282
  29. lemma OAI.CriticalStrip.Diagram.interpolationNumerator_collision line 293
  30. lemma OAI.CriticalStrip.Diagram.functionMatrix_ring_map line 307
  31. def OAI.CriticalStrip.Diagram.deletionMapL line 313
  32. lemma OAI.CriticalStrip.Diagram.deletionMapL_map line 319
  33. def OAI.CriticalStrip.Diagram.nodalHeadL line 328
  34. lemma OAI.CriticalStrip.Diagram.nodalHeadL_map line 333
  35. def OAI.CriticalStrip.Diagram.reflectionFactorL line 350
  36. lemma OAI.CriticalStrip.Diagram.reflectionFactorL_map line 353
  37. def OAI.CriticalStrip.Diagram.nodalDatumL line 366
  38. lemma OAI.CriticalStrip.Diagram.nodalDatumL_map line 372
  39. lemma OAI.CriticalStrip.Diagram.LaurentBox.cosine line 395
  40. lemma OAI.CriticalStrip.Diagram.LaurentBox.pow line 401
  41. lemma OAI.CriticalStrip.Diagram.LaurentBox.insert line 414
  42. lemma OAI.CriticalStrip.Diagram.LaurentMatrixBox.mulVec line 425
  43. lemma OAI.CriticalStrip.Diagram.functionMatrix_box line 432
  44. lemma OAI.CriticalStrip.Diagram.LaurentMatrixBox.mono line 440
  45. def OAI.CriticalStrip.Diagram.pairBound line 450
  46. def OAI.CriticalStrip.Diagram.selfBound line 452
  47. lemma OAI.CriticalStrip.Diagram.pairBound_add line 454
  48. lemma OAI.CriticalStrip.Diagram.pairBound_sub line 460
  49. lemma OAI.CriticalStrip.Diagram.sum_pairBound line 466
  50. lemma OAI.CriticalStrip.Diagram.reflectionFactorL_box line 479
  51. lemma OAI.CriticalStrip.Diagram.reducedMovingStepL_box line 490
  52. lemma OAI.CriticalStrip.Diagram.nodalHeadL_box line 515
  53. lemma OAI.CriticalStrip.Diagram.deletionMapL_box line 531
  54. lemma OAI.CriticalStrip.Diagram.nodalDatumL_box line 543