OAI/Combinatorics/StripMass/LaguerreNormalization.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.integral_laguerreOddIntegrand line 14
  2. lemma OAI.CriticalStrip.laguerre_doubleIntegrand_eq line 34
  3. lemma OAI.CriticalStrip.integrable_laguerre_doubleIntegrand line 42
  4. lemma OAI.CriticalStrip.laguerre_doubleMomentMatrix_eq line 52
  5. lemma OAI.CriticalStrip.laguerre_singleMoment_eq line 59
  6. theorem OAI.CriticalStrip.laguerreNormalizer_eq_product line 66
  7. lemma OAI.Matrix.sum_det_updateRow_mul line 110
  8. def OAI.CriticalStrip.gammaPhi line 140
  9. def OAI.CriticalStrip.gammaSchurProduct line 142
  10. lemma OAI.CriticalStrip.gammaSchurProduct_eq line 145
  11. lemma OAI.CriticalStrip.gammaPhi_doubleIntegrand_eq line 151
  12. lemma OAI.CriticalStrip.gammaPhi_doubleMomentMatrix_eq line 159
  13. lemma OAI.CriticalStrip.integrable_gammaPhi_doubleIntegrand line 170
  14. lemma OAI.CriticalStrip.gammaPhi_singleMoment_eq line 178
  15. theorem OAI.CriticalStrip.integral_gamma_determinant_schur line 186
  16. def OAI.CriticalStrip.inverseExponents line 268
  17. lemma OAI.CriticalStrip.inverseExponents_pos line 271
  18. lemma OAI.CriticalStrip.inverseExponents_strictMono line 279
  19. lemma OAI.CriticalStrip.laguerreWeight_add_one line 289
  20. lemma OAI.CriticalStrip.inverseExponents_determinant line 293
  21. lemma OAI.CriticalStrip.integrableOn_laguerre_inverseSum line 323
  22. lemma OAI.CriticalStrip.integral_laguerre_inverseSum_eq_gammaProduct line 334
  23. lemma OAI.CriticalStrip.orderedPairProduct_cons line 346
  24. lemma OAI.CriticalStrip.gammaSchurProduct_cons line 364
  25. lemma OAI.CriticalStrip.gammaSchurProduct_laguerre line 372
  26. lemma OAI.CriticalStrip.laguerreNormalizer_succ_product line 382
  27. lemma OAI.CriticalStrip.gammaSchurProduct_inverse line 400
  28. lemma OAI.CriticalStrip.telescoping_inverse_product line 416