OAI/Combinatorics/StripMass/SchurIdentity.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.StripPfaffian.pfaffian_schur_even line 12
  2. lemma OAI.StripPfaffian.pfaffian_schur_odd_snoc line 49
  3. theorem OAI.StripPfaffian.pfaffian_schur_odd line 68
  4. lemma OAI.CriticalStrip.integral_translate_Ioi line 99
  5. lemma OAI.CriticalStrip.integral_shifted_rpow line 107
  6. lemma OAI.CriticalStrip.ae_pos_pair line 120
  7. def OAI.CriticalStrip.gammaLaplace line 125
  8. lemma OAI.CriticalStrip.measurable_gammaLaplace line 129
  9. lemma OAI.CriticalStrip.integrable_gammaLaplace_section line 133
  10. lemma OAI.CriticalStrip.integral_gammaLaplace_section line 138
  11. lemma OAI.CriticalStrip.integrable_gammaFraction line 145
  12. lemma OAI.CriticalStrip.integrable_gammaLaplace line 157
  13. lemma OAI.CriticalStrip.gammaLaplace_factor line 173
  14. lemma OAI.CriticalStrip.integral_gammaLaplace_pair line 193
  15. lemma OAI.CriticalStrip.integral_gammaFraction line 215
  16. def OAI.CriticalStrip.gammaSkewIntegrand line 234
  17. lemma OAI.CriticalStrip.gammaSkewIntegrand_eq line 237
  18. lemma OAI.CriticalStrip.integrable_gammaSkewIntegrand line 245
  19. lemma OAI.CriticalStrip.integral_gammaSkewIntegrand line 251
  20. theorem OAI.CriticalStrip.laguerre_double_moment line 269
  21. lemma OAI.StripPfaffian.border_scale_coordinates line 286
  22. lemma OAI.StripPfaffian.pfaffian_border_scale_coordinates line 296
  23. theorem OAI.StripPfaffian.pfaffian_weighted_schur_even line 306
  24. theorem OAI.StripPfaffian.pfaffian_weighted_schur_odd line 314
  25. def OAI.CriticalStrip.laguerreMomentMatrix line 333
  26. def OAI.CriticalStrip.laguerreMomentColumn line 336
  27. def OAI.CriticalStrip.laguerreNormalizerProduct line 341
  28. lemma OAI.CriticalStrip.laguerreMomentMatrix_eq line 345
  29. lemma OAI.CriticalStrip.laguerreMomentColumn_eq line 359
  30. lemma OAI.CriticalStrip.laguerre_schur_denominators line 364
  31. lemma OAI.CriticalStrip.laguerre_schur_injective line 369
  32. lemma OAI.CriticalStrip.laguerreNormalizerProduct_eq line 376
  33. theorem OAI.CriticalStrip.laguerreMomentMatrix_pfaffian_even line 393
  34. theorem OAI.CriticalStrip.laguerreMomentMatrix_pfaffian_odd line 399
  35. lemma OAI.StripPfaffian.sum_pow_list line 415
  36. lemma OAI.StripPfaffian.ofFn_smul_prod line 430