OAI/Combinatorics/StripMass/PfaffianIntegration.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.StripPfaffian.integral_pair_single_product line 13
  2. lemma OAI.StripPfaffian.integrable_pair_single_product line 27
  3. def OAI.StripPfaffian.singleMoment line 43
  4. lemma OAI.StripPfaffian.product_double_singleIntegrand line 47
  5. lemma OAI.StripPfaffian.determinant_times_oddPairs line 59
  6. lemma OAI.StripPfaffian.integrable_determinant_times_oddPairs line 73
  7. lemma OAI.StripPfaffian.integral_determinant_times_oddPairs line 83
  8. theorem OAI.StripPfaffian.deBruijn_odd line 105
  9. lemma OAI.CriticalStrip.laguerreDomain_subset_positive line 175
  10. lemma OAI.CriticalStrip.positive_product_restrict_chamber line 179
  11. lemma OAI.CriticalStrip.ae_positive_product line 186
  12. lemma OAI.CriticalStrip.sum_ordered_indicator line 192
  13. lemma OAI.CriticalStrip.integral_symmetric_ordered line 221
  14. lemma OAI.StripPfaffian.permMap_apply line 260
  15. lemma OAI.StripPfaffian.pfaffian_border_perm line 275
  16. lemma OAI.StripPfaffian.perm_sign_mul_self line 293
  17. lemma OAI.StripPfaffian.determinantPfaffian_symmetric_even line 299
  18. lemma OAI.StripPfaffian.determinantPfaffian_symmetric_odd line 313
  19. lemma OAI.StripPfaffian.evaluationMatrix_det_of_not_injective line 331
  20. def OAI.CriticalStrip.laguerrePhi line 347
  21. lemma OAI.CriticalStrip.laguerreWeight_shift_nat line 349
  22. lemma OAI.CriticalStrip.laguerre_evaluation_determinant line 355
  23. lemma OAI.CriticalStrip.vandermonde_schur_density line 369
  24. def OAI.CriticalStrip.laguerreEvenIntegrand line 386
  25. def OAI.CriticalStrip.laguerreOddIntegrand line 390
  26. lemma OAI.CriticalStrip.laguerreEvenIntegrand_eq line 394
  27. lemma OAI.CriticalStrip.laguerreOddIntegrand_eq line 404
  28. lemma OAI.CriticalStrip.integral_laguerreEvenIntegrand line 414