OAI/Combinatorics/StripMass/LaurentBox.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.LaurentBox line 15
  2. lemma OAI.CriticalStrip.Diagram.LaurentBox.zero line 18
  3. lemma OAI.CriticalStrip.Diagram.LaurentBox.mono line 22
  4. lemma OAI.CriticalStrip.Diagram.LaurentBox.add line 29
  5. lemma OAI.CriticalStrip.Diagram.LaurentBox.neg line 36
  6. lemma OAI.CriticalStrip.Diagram.LaurentBox.sub line 41
  7. lemma OAI.CriticalStrip.Diagram.LaurentBox.mul line 46
  8. lemma OAI.CriticalStrip.Diagram.LaurentBox.single line 58
  9. lemma OAI.CriticalStrip.Diagram.LaurentBox.constant line 67
  10. lemma OAI.CriticalStrip.Diagram.LaurentBox.one line 70
  11. lemma OAI.CriticalStrip.Diagram.LaurentBox.sine line 74
  12. lemma OAI.CriticalStrip.Diagram.LaurentBox.sum line 81
  13. lemma OAI.CriticalStrip.Diagram.LaurentBox.prod line 89
  14. lemma OAI.CriticalStrip.Diagram.laurent_mul_top_coeff line 109
  15. lemma OAI.CriticalStrip.Diagram.laurent_mul_bottom_coeff line 128
  16. theorem OAI.CriticalStrip.Diagram.LaurentInterval.quotient line 149
  17. lemma OAI.CriticalStrip.Diagram.peelLaurentEquiv_coeff_coeff line 183
  18. lemma OAI.CriticalStrip.Diagram.peelLaurent_coeff line 190
  19. lemma OAI.CriticalStrip.Diagram.peelLaurent_coeff_ne_zero_iff line 194
  20. lemma OAI.CriticalStrip.Diagram.LaurentBox.peel line 212
  21. lemma OAI.CriticalStrip.Diagram.LaurentBox.of_peel line 218
  22. lemma OAI.CriticalStrip.Diagram.laurent_linear_dvd line 236
  23. lemma OAI.CriticalStrip.Diagram.laurent_eval_linear line 251
  24. lemma OAI.CriticalStrip.Diagram.laurent_prod_linear_dvd line 258
  25. theorem OAI.CriticalStrip.Diagram.prod_dvd_of_evaluation_packets line 290
  26. lemma OAI.CriticalStrip.Diagram.laurent_prod_linear_indexed_dvd line 312
  27. def OAI.CriticalStrip.Diagram.monomialUnit line 331
  28. lemma OAI.CriticalStrip.Diagram.peelLaurentEquiv_insert line 337
  29. def OAI.CriticalStrip.Diagram.substituteLaurent line 349
  30. lemma OAI.CriticalStrip.Diagram.substituteLaurent_insert line 353
  31. def OAI.CriticalStrip.Diagram.cosineCollisionRoots line 360
  32. def OAI.CriticalStrip.Diagram.cosineCollisionPacket line 363
  33. lemma OAI.CriticalStrip.Diagram.cosineCollision_factorization line 368
  34. lemma OAI.CriticalStrip.Diagram.cosineCollisionPacket_dvd line 391
  35. theorem OAI.CriticalStrip.Diagram.pairFirst_injective line 408
  36. theorem OAI.CriticalStrip.Diagram.pairSecond_injective line 415
  37. theorem OAI.CriticalStrip.Diagram.upperPair_incident_iff line 422
  38. theorem OAI.CriticalStrip.Diagram.pairIndex_unique line 427
  39. theorem OAI.CriticalStrip.Diagram.selectedPairs_incident_unique line 438
  40. theorem OAI.CriticalStrip.Diagram.pairIndex_cover line 450
  41. def OAI.CriticalStrip.Diagram.firstPair line 465
  42. theorem OAI.CriticalStrip.Diagram.firstPair_eq_upperPair line 469
  43. def OAI.CriticalStrip.Diagram.repairFirstDenominator line 475
  44. def OAI.CriticalStrip.Diagram.isolateFirstNumerator line 481
  45. theorem OAI.CriticalStrip.Diagram.isolateFirstNumerator_selected line 486
  46. theorem OAI.CriticalStrip.Diagram.repairFirstDenominator_compl line 507