OAI/Combinatorics/StripMass/DiagonalFactors.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.separateCosine line 17
  2. theorem OAI.CriticalStrip.Diagram.separateCosine_C line 22
  3. theorem OAI.CriticalStrip.Diagram.separateCosine_self line 26
  4. theorem OAI.CriticalStrip.Diagram.separateCosine_other line 30
  5. def OAI.CriticalStrip.Diagram.cosineDiagonalEval line 34
  6. theorem OAI.CriticalStrip.Diagram.cosineDiagonalEval_C line 38
  7. theorem OAI.CriticalStrip.Diagram.cosineDiagonalEval_self line 42
  8. theorem OAI.CriticalStrip.Diagram.cosineDiagonalEval_other line 46
  9. theorem OAI.CriticalStrip.Diagram.cosineDiagonalEval_swap line 51
  10. theorem OAI.CriticalStrip.Diagram.prime_cosine_difference line 62
  11. theorem OAI.CriticalStrip.Diagram.cosine_difference_dvd_of_swap line 70
  12. theorem OAI.CriticalStrip.Diagram.cosine_differences_relPrime line 91
  13. theorem OAI.CriticalStrip.Diagram.scalarNumerator_vandermonde_dvd line 117
  14. def OAI.CriticalStrip.Diagram.sourceVandermonde line 137
  15. theorem OAI.CriticalStrip.Diagram.sourceVandermonde_ne_zero line 140
  16. theorem OAI.CriticalStrip.Diagram.sourceVandermonde_eq_det line 146
  17. theorem OAI.CriticalStrip.Diagram.sourceVandermonde_reindex line 151
  18. theorem OAI.CriticalStrip.Diagram.map_sourceVandermonde line 160
  19. def OAI.CriticalStrip.Diagram.scalarPolynomial line 167
  20. theorem OAI.CriticalStrip.Diagram.scalarNumerator_eq_vandermonde line 170
  21. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_eval line 176
  22. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_rename line 190
  23. lemma OAI.CriticalStrip.Diagram.scalarNormalization_quotient line 217
  24. lemma OAI.CriticalStrip.Diagram.scalarNormalization_reindex line 225
  25. lemma OAI.CriticalStrip.Diagram.map_pfaffian line 237
  26. lemma OAI.CriticalStrip.Diagram.map_augmentedKernel line 243
  27. lemma OAI.CriticalStrip.Diagram.map_scalarNormalization line 251
  28. lemma OAI.CriticalStrip.Diagram.permSpectral_normalization line 257
  29. def OAI.CriticalStrip.Diagram.insertExponent line 273
  30. lemma OAI.CriticalStrip.Diagram.insertExponent_injective line 278
  31. def OAI.CriticalStrip.Diagram.insertLaurent line 283
  32. lemma OAI.CriticalStrip.Diagram.insertLaurent_injective line 286
  33. def OAI.CriticalStrip.Diagram.insertSpectral line 289
  34. lemma OAI.CriticalStrip.Diagram.insertSpectral_evalLaurent line 295
  35. lemma OAI.CriticalStrip.Diagram.insertLaurent_monomial line 299
  36. lemma OAI.CriticalStrip.Diagram.insertSpectral_const line 303
  37. lemma OAI.CriticalStrip.Diagram.insertSpectral_variable line 312
  38. lemma OAI.CriticalStrip.Diagram.insertSpectral_torusSin line 322
  39. lemma OAI.CriticalStrip.Diagram.insertSpectral_torusCos line 326
  40. lemma OAI.CriticalStrip.Diagram.insertSpectral_torusL line 330
  41. lemma OAI.CriticalStrip.Diagram.insertSpectral_torusWeights line 333
  42. lemma OAI.CriticalStrip.Diagram.insertSpectral_spectralWeights line 337
  43. lemma OAI.CriticalStrip.Diagram.insertSpectral_spectralA line 341
  44. lemma OAI.CriticalStrip.Diagram.insertSpectral_vacuum line 344
  45. lemma OAI.CriticalStrip.Diagram.insertSpectral_normalization line 350
  46. def OAI.CriticalStrip.Diagram.peelExponent line 365
  47. def OAI.CriticalStrip.Diagram.peelLaurentEquiv line 372
  48. lemma OAI.CriticalStrip.Diagram.peelLaurentEquiv_monomial line 377
  49. def OAI.CriticalStrip.Diagram.peelLaurent line 387
  50. lemma OAI.CriticalStrip.Diagram.peelLaurent_injective line 392
  51. lemma OAI.CriticalStrip.Diagram.peelLaurent_monomial line 396
  52. lemma OAI.CriticalStrip.Diagram.peelLaurent_insert line 403
  53. lemma OAI.CriticalStrip.Diagram.peelLaurent_variable line 415
  54. instance OAI.CriticalStrip.Diagram.peeledRingIsDomain line 426
  55. abbrev OAI.CriticalStrip.Diagram.SingleSpectral line 429
  56. instance OAI.CriticalStrip.Diagram.singleSpectralField line 431
  57. def OAI.CriticalStrip.Diagram.peelSpectral line 433
  58. lemma OAI.CriticalStrip.Diagram.peelSpectral_evalLaurent line 438
  59. def OAI.CriticalStrip.Diagram.singleCoeff line 443
  60. lemma OAI.CriticalStrip.Diagram.peelSpectral_insert line 446
  61. def OAI.CriticalStrip.Diagram.LaurentInterval line 470
  62. lemma OAI.CriticalStrip.Diagram.laurent_trunc_coeff line 473
  63. lemma OAI.CriticalStrip.Diagram.laurent_toLaurent_coeff line 476
  64. lemma OAI.CriticalStrip.Diagram.laurent_toLaurent_negative line 481
  65. lemma OAI.CriticalStrip.Diagram.laurent_toLaurent_trunc line 490
  66. lemma OAI.CriticalStrip.Diagram.laurent_shift_coeff line 499
  67. lemma OAI.CriticalStrip.Diagram.LaurentInterval.shift line 504
  68. lemma OAI.CriticalStrip.Diagram.LaurentInterval.shift_trunc line 512
  69. theorem OAI.CriticalStrip.Diagram.laurent_root_saturation line 524