OAI/Combinatorics/StripMass/PfaffianRecursion.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.StripPfaffian.pfaffian_border line 13
  2. lemma OAI.StripPfaffian.topCoord_embed_twice line 33
  3. lemma OAI.StripPfaffian.pfaffian_block_pair line 48
  4. lemma OAI.StripPfaffian.borderLinear_column line 67
  5. lemma OAI.StripPfaffian.basis_last line 81
  6. lemma OAI.StripPfaffian.pfaffian_zero_row line 85
  7. lemma OAI.StripPfaffian.pfaffian_block_extra line 120
  8. def OAI.StripPfaffian.lastSwap line 138
  9. lemma OAI.StripPfaffian.lastSwap_old line 141
  10. lemma OAI.StripPfaffian.lastSwap_middle line 148
  11. lemma OAI.StripPfaffian.lastSwap_last line 150
  12. lemma OAI.StripPfaffian.lastSwap_symm line 152
  13. lemma OAI.StripPfaffian.border_swap_matrix line 154
  14. lemma OAI.StripPfaffian.pfaffian_border_swap line 167
  15. lemma OAI.StripPfaffian.pfaffian_aug_pair line 176
  16. lemma OAI.StripPfaffian.borderLinear_aug_ones line 185
  17. lemma OAI.StripPfaffian.D_symm line 199
  18. lemma OAI.StripPfaffian.kernel_skew line 200
  19. lemma OAI.StripPfaffian.kernel_self line 204
  20. def OAI.StripPfaffian.kernelMatrix line 206
  21. lemma OAI.StripPfaffian.kernelMatrix_skew line 209
  22. lemma OAI.StripPfaffian.kernelMatrix_snoc line 212
  23. lemma OAI.StripPfaffian.augmentedKernel_skew line 220
  24. def OAI.StripPfaffian.actualPf line 226
  25. lemma OAI.StripPfaffian.pfaffian_cast line 228
  26. lemma OAI.StripPfaffian.actualPf_even line 233
  27. lemma OAI.StripPfaffian.actualPf_odd line 242
  28. lemma OAI.StripPfaffian.actualPf_duplicate line 253
  29. def OAI.StripPfaffian.restrictMap line 267
  30. def OAI.StripPfaffian.flipLastMap line 272
  31. lemma OAI.StripPfaffian.restrictMap_snoc line 277
  32. lemma OAI.StripPfaffian.flipLastMap_snoc line 279
  33. def OAI.StripPfaffian.incrementLinear line 282
  34. lemma OAI.StripPfaffian.incrementLinear_eval line 287
  35. lemma OAI.StripPfaffian.incrementLinear_leading line 303
  36. def OAI.StripPfaffian.polyLift line 319
  37. lemma OAI.StripPfaffian.linear_basis_sum line 322
  38. lemma OAI.StripPfaffian.polyLift_eval line 327
  39. lemma OAI.StripPfaffian.polyLift_coeff line 332
  40. lemma OAI.StripPfaffian.polyLift_degree line 337
  41. def OAI.StripPfaffian.Dpoly line 343
  42. def OAI.StripPfaffian.pairNumerator line 344
  43. def OAI.StripPfaffian.denominatorPoly line 345
  44. def OAI.StripPfaffian.deletedDenominator line 346
  45. def OAI.StripPfaffian.kernelNumerator line 348
  46. def OAI.StripPfaffian.clearedPf line 351
  47. lemma OAI.StripPfaffian.Dpoly_eval line 354
  48. lemma OAI.StripPfaffian.Dpoly_degree line 355
  49. lemma OAI.StripPfaffian.Dpoly_coeff line 356
  50. lemma OAI.StripPfaffian.pairNumerator_degree line 359
  51. lemma OAI.StripPfaffian.pairNumerator_coeff line 362
  52. lemma OAI.StripPfaffian.denominatorPoly_degree line 367
  53. lemma OAI.StripPfaffian.denominatorPoly_coeff line 374
  54. lemma OAI.StripPfaffian.deletedDenominator_degree line 380
  55. lemma OAI.StripPfaffian.deletedDenominator_coeff line 387
  56. lemma OAI.StripPfaffian.kernelNumerator_degree line 393
  57. lemma OAI.StripPfaffian.kernelNumerator_coeff line 401
  58. lemma OAI.StripPfaffian.clearedPf_degree line 409
  59. lemma OAI.StripPfaffian.clearedPf_coeff line 416
  60. lemma OAI.StripPfaffian.denominatorPoly_eval line 424
  61. lemma OAI.StripPfaffian.deletedDenominator_mul line 427
  62. lemma OAI.StripPfaffian.kernelNumerator_eval line 431