OAI/Combinatorics/StripMass/InverseIntegrability.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.integrableOn_scaledLaguerre_inverse_coordinate line 13
  2. abbrev OAI.CriticalStrip.mobiusInverseQuarter line 26
  3. lemma OAI.CriticalStrip.continuousOn_mobiusInverseQuarter line 29
  4. lemma OAI.CriticalStrip.antitoneOn_mobiusInverseQuarter line 34
  5. lemma OAI.CriticalStrip.integrableOn_scaledLaguerre_mobiusInverseQuarter line 40
  6. lemma OAI.CriticalStrip.positiveLaw_mobius_expectation line 58
  7. theorem OAI.CriticalStrip.positiveLaw_inverseQuarter_ge_scaled_reference line 70
  8. lemma OAI.CriticalStrip.integral_scaledLaguerre_cutoff_inverse_coordinate line 126
  9. lemma OAI.CriticalStrip.scaled_reference_cutoff_inverse_coordinate line 144
  10. theorem OAI.CriticalStrip.positiveLaw_inverseQuarter_ge_reference line 157
  11. lemma OAI.StripPfaffian.congruence_skew line 196
  12. lemma OAI.StripPfaffian.toLin_basis line 210
  13. lemma OAI.StripPfaffian.sum_four_reverse line 216
  14. lemma OAI.StripPfaffian.twoForm_congruence line 226
  15. lemma OAI.StripPfaffian.pfaffian_congruence line 248
  16. lemma OAI.StripPfaffian.pfaffian_scale_coordinates line 266
  17. def OAI.StripPfaffian.schurComplement line 276
  18. lemma OAI.StripPfaffian.schurComplement_skew line 279
  19. def OAI.StripPfaffian.eliminatingShear line 286
  20. lemma OAI.StripPfaffian.eliminatingShear_upper line 293
  21. lemma OAI.StripPfaffian.eliminatingShear_det line 307
  22. lemma OAI.StripPfaffian.eliminatingShear_congruence line 313
  23. lemma OAI.StripPfaffian.pfaffian_schur_complement line 328
  24. def OAI.StripPfaffian.schurEntry line 345
  25. def OAI.StripPfaffian.schurMatrix line 346
  26. def OAI.StripPfaffian.schurProduct line 348
  27. lemma OAI.StripPfaffian.schurEntry_self line 351
  28. lemma OAI.StripPfaffian.schurEntry_swap line 352
  29. lemma OAI.StripPfaffian.schurMatrix_skew line 355
  30. lemma OAI.StripPfaffian.schurEntry_ne_zero line 358
  31. lemma OAI.StripPfaffian.schurEntry_elimination line 361
  32. lemma OAI.StripPfaffian.schurEntry_border_elimination line 374
  33. lemma OAI.StripPfaffian.schurMatrix_snoc line 382
  34. lemma OAI.StripPfaffian.schurColumn_snoc line 391
  35. lemma OAI.StripPfaffian.schurProduct_snoc line 397
  36. lemma OAI.StripPfaffian.pfaffian_empty line 404
  37. lemma OAI.StripPfaffian.pfaffian_schur_snoc_snoc line 409