OAI/Combinatorics/StripMass/RestrictedDiagrams.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.rawRestricted line 11
  2. theorem OAI.CriticalStrip.Diagram.column_eq_raw line 15
  3. theorem OAI.CriticalStrip.Diagram.rawColumn_scale line 18
  4. theorem OAI.CriticalStrip.Diagram.rawColumn_map line 28
  5. theorem OAI.CriticalStrip.Diagram.rawRestricted_scale line 38
  6. theorem OAI.CriticalStrip.Diagram.rawRestricted_map line 45
  7. theorem OAI.CriticalStrip.Diagram.cleared_map line 52
  8. theorem OAI.CriticalStrip.Diagram.regular_of_cleared_specialization line 75
  9. abbrev OAI.CriticalStrip.Diagram.Laurent line 107
  10. abbrev OAI.CriticalStrip.Diagram.SpectralRing line 108
  11. abbrev OAI.CriticalStrip.Diagram.SpectralField line 109
  12. def OAI.CriticalStrip.Diagram.constF line 111
  13. def OAI.CriticalStrip.Diagram.variableExponent line 113
  14. def OAI.CriticalStrip.Diagram.variableF line 116
  15. def OAI.CriticalStrip.Diagram.phase line 120
  16. def OAI.CriticalStrip.Diagram.rho line 121
  17. def OAI.CriticalStrip.Diagram.d line 122
  18. def OAI.CriticalStrip.Diagram.C line 123
  19. def OAI.CriticalStrip.Diagram.torusSin line 125
  20. def OAI.CriticalStrip.Diagram.torusCos line 128
  21. def OAI.CriticalStrip.Diagram.torusL line 130
  22. def OAI.CriticalStrip.Diagram.torusWeights line 134
  23. def OAI.CriticalStrip.Diagram.spectralWeights line 145
  24. def OAI.CriticalStrip.Diagram.spectralA line 148
  25. def OAI.CriticalStrip.Diagram.discriminant line 151
  26. def OAI.CriticalStrip.Diagram.pairFirst line 154
  27. def OAI.CriticalStrip.Diagram.pairSecond line 155
  28. def OAI.CriticalStrip.Diagram.pfaffian line 157
  29. def OAI.CriticalStrip.Diagram.augmentedKernel line 163
  30. def OAI.CriticalStrip.Diagram.scalarNormalization line 172
  31. def OAI.CriticalStrip.Diagram.spectralNormalization line 176
  32. def OAI.CriticalStrip.Diagram.evalLaurent line 180
  33. def OAI.CriticalStrip.Diagram.liftLaurent line 183
  34. def OAI.CriticalStrip.Diagram.lastExponent line 186
  35. def OAI.CriticalStrip.Diagram.lastCosine line 188
  36. def OAI.CriticalStrip.Diagram.lastSine line 192
  37. def OAI.CriticalStrip.Diagram.PolynomialVacuum line 198
  38. def OAI.CriticalStrip.Diagram.monomialL line 215
  39. def OAI.CriticalStrip.Diagram.constantL line 218
  40. def OAI.CriticalStrip.Diagram.flatEval line 220
  41. theorem OAI.CriticalStrip.Diagram.flatEval_monomial line 223
  42. theorem OAI.CriticalStrip.Diagram.flatEval_constant line 227
  43. theorem OAI.CriticalStrip.Diagram.monomialL_mul line 230
  44. theorem OAI.CriticalStrip.Diagram.monomialL_zero_one line 234
  45. theorem OAI.CriticalStrip.Diagram.map_constantL line 237
  46. theorem OAI.CriticalStrip.Diagram.map_monomialL_inv line 241
  47. def OAI.CriticalStrip.Diagram.sineL line 248
  48. theorem OAI.CriticalStrip.Diagram.sineL_map line 251
  49. theorem OAI.CriticalStrip.Diagram.flatEval_sine line 258
  50. theorem OAI.CriticalStrip.Diagram.phase_ne_zero line 262
  51. theorem OAI.CriticalStrip.Diagram.phase_pow line 264
  52. theorem OAI.CriticalStrip.Diagram.phase_sine line 269
  53. theorem OAI.CriticalStrip.Diagram.flatEval_sine_phase line 277
  54. theorem OAI.CriticalStrip.Diagram.variableF_ne_zero line 281
  55. theorem OAI.CriticalStrip.Diagram.map_monomialL_factor line 285
  56. theorem OAI.CriticalStrip.Diagram.map_monomialL_variable line 293
  57. theorem OAI.CriticalStrip.Diagram.map_monomialL_neg_variable line 297
  58. theorem OAI.CriticalStrip.Diagram.constF_phase_ne_zero line 306
  59. theorem OAI.CriticalStrip.Diagram.map_sine_variable line 309
  60. theorem OAI.CriticalStrip.Diagram.map_sine_neg_variable line 316
  61. theorem OAI.CriticalStrip.Diagram.map_sine_variable_nat line 323
  62. theorem OAI.CriticalStrip.Diagram.map_sine_neg_variable_nat line 330
  63. def OAI.CriticalStrip.Diagram.rowDenominator line 339
  64. def OAI.CriticalStrip.Diagram.rowNumerator line 343
  65. theorem OAI.CriticalStrip.Diagram.inlinePrivate0_sin_five_lambda line 358
  66. theorem OAI.CriticalStrip.Diagram.inlinePrivate0_sin_six_lambda line 360
  67. theorem OAI.CriticalStrip.Diagram.flatEval_rowDenominator line 363
  68. theorem OAI.CriticalStrip.Diagram.flatEval_rowDenominator_ne_zero line 370
  69. theorem OAI.CriticalStrip.Diagram.rowDenominator_map line 376
  70. theorem OAI.CriticalStrip.Diagram.rowDenominator_map_ne_zero line 382
  71. theorem OAI.CriticalStrip.Diagram.rowNumerator_flatEval line 388
  72. theorem OAI.CriticalStrip.Diagram.rowNumerator_map line 398
  73. theorem OAI.CriticalStrip.Diagram.spectral_regular line 424
  74. theorem OAI.CriticalStrip.Diagram.spectral_normalizedVacuum_stationary line 438