OAI/Combinatorics/StripMass/PairCoordinates.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.StripPfaffian.pairArrayEquiv line 12
  2. def OAI.StripPfaffian.pairLeft line 17
  3. def OAI.StripPfaffian.pairRight line 18
  4. lemma OAI.StripPfaffian.pairArrayEquiv_apply line 20
  5. lemma OAI.StripPfaffian.pair_wedge_product line 23
  6. lemma OAI.StripPfaffian.twoForm_pow_expansion line 31
  7. def OAI.StripPfaffian.permInjectiveEquiv line 50
  8. lemma OAI.StripPfaffian.sum_basis_determinant line 57
  9. def OAI.StripPfaffian.pairEntries line 79
  10. theorem OAI.StripPfaffian.pfaffian_permutation_expansion line 84
  11. lemma OAI.StripPfaffian.pairArrayEquiv_symm_left line 106
  12. lemma OAI.StripPfaffian.pairArrayEquiv_symm_right line 110
  13. def OAI.StripPfaffian.pairArrayMeasurableEquiv line 114
  14. lemma OAI.StripPfaffian.pairArray_preimage_pi line 134
  15. lemma OAI.StripPfaffian.measurePreserving_pairArray line 150
  16. lemma OAI.StripPfaffian.integral_pair_product line 169
  17. lemma OAI.StripPfaffian.integrable_pair_product line 176
  18. lemma OAI.StripPfaffian.prod_pairs line 184
  19. lemma OAI.StripPfaffian.piCongrLeft_const_apply line 189
  20. lemma OAI.StripPfaffian.integral_alternating_times_perm line 196
  21. lemma OAI.StripPfaffian.integrable_alternating_times_perm line 210
  22. def OAI.StripPfaffian.evaluationMatrix line 224
  23. def OAI.StripPfaffian.doubleIntegrand line 227
  24. def OAI.StripPfaffian.doubleMomentMatrix line 230
  25. lemma OAI.StripPfaffian.doubleMomentMatrix_skew line 234
  26. lemma OAI.StripPfaffian.evaluationMatrix_det_perm line 246
  27. lemma OAI.StripPfaffian.product_doubleIntegrand line 251
  28. lemma OAI.StripPfaffian.determinant_times_pairs line 261
  29. lemma OAI.StripPfaffian.integrable_determinant_times_pairs line 274
  30. lemma OAI.StripPfaffian.integral_determinant_times_pairs line 282
  31. theorem OAI.StripPfaffian.deBruijn_even line 298
  32. lemma OAI.StripPfaffian.borderLinear_eq_topCoord line 357
  33. def OAI.StripPfaffian.oddPairEntries line 374
  34. lemma OAI.StripPfaffian.wedge_snoc line 378
  35. lemma OAI.StripPfaffian.twoForm_pow_mul_expansion line 384
  36. theorem OAI.StripPfaffian.pfaffian_border_permutation_expansion line 408