OAI/Combinatorics/StripMass/CramerBounds.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.betaL_box line 14
  2. lemma OAI.CriticalStrip.Diagram.LaurentMatrixBox.det_terms line 19
  3. lemma OAI.CriticalStrip.Diagram.interpolationNumerator_box line 35
  4. lemma OAI.CriticalStrip.Diagram.constants_extreme_nonzero line 85
  5. lemma OAI.CriticalStrip.Diagram.beta_difference_box line 91
  6. lemma OAI.CriticalStrip.Diagram.beta_difference_exact line 101
  7. lemma OAI.CriticalStrip.Diagram.vandermonde_beta_exact line 136
  8. def OAI.CriticalStrip.Diagram.inlinePrivate155_signMonomial line 160
  9. def OAI.CriticalStrip.Diagram.signLaurent line 168
  10. lemma OAI.CriticalStrip.Diagram.signLaurent_monomial line 171
  11. lemma OAI.CriticalStrip.Diagram.signLaurent_involutive line 178
  12. def OAI.CriticalStrip.Diagram.signSpectral line 187
  13. lemma OAI.CriticalStrip.Diagram.signSpectral_evalLaurent line 193
  14. lemma OAI.CriticalStrip.Diagram.signSpectral_const line 197
  15. lemma OAI.CriticalStrip.Diagram.signSpectral_variable line 205
  16. lemma OAI.CriticalStrip.Diagram.signSpectral_torusSin line 220
  17. lemma OAI.CriticalStrip.Diagram.signSpectral_torusCos line 224
  18. lemma OAI.CriticalStrip.Diagram.signSpectral_torusL line 228
  19. lemma OAI.CriticalStrip.Diagram.signSpectral_torusWeights line 231
  20. def OAI.CriticalStrip.Diagram.occupancySign line 246
  21. def OAI.CriticalStrip.Diagram.Weights.signTwist line 249
  22. lemma OAI.CriticalStrip.Diagram.occupancySign_empty line 252
  23. lemma OAI.CriticalStrip.Diagram.occupancySign_mul_self line 254
  24. def OAI.CriticalStrip.Diagram.inlinePrivate156_tileWest line 258
  25. def OAI.CriticalStrip.Diagram.inlinePrivate156_tileEast line 261
  26. lemma OAI.CriticalStrip.Diagram.inlinePrivate156_tileWest_iff line 264
  27. lemma OAI.CriticalStrip.Diagram.inlinePrivate156_tileEast_iff line 266
  28. lemma OAI.CriticalStrip.Diagram.Weights.signTwist_tile line 269
  29. lemma OAI.CriticalStrip.Diagram.column_signTwist line 275
  30. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_signTwist line 296
  31. lemma OAI.CriticalStrip.Diagram.torusL_neg line 330
  32. lemma OAI.CriticalStrip.Diagram.torusWeights_neg line 334
  33. lemma OAI.CriticalStrip.Diagram.signSpectral_spectralA line 340
  34. lemma OAI.CriticalStrip.Diagram.signSpectral_spectralWeights line 346
  35. lemma OAI.CriticalStrip.Diagram.signSpectral_vacuum line 360
  36. lemma OAI.CriticalStrip.Diagram.signSpectral_normalization line 370
  37. theorem OAI.CriticalStrip.Diagram.rationalVacuum_sign line 376
  38. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_gauge line 389
  39. lemma OAI.CriticalStrip.Diagram.spectral_div_neg line 416
  40. def OAI.CriticalStrip.Diagram.doubleSignTwist line 419
  41. lemma OAI.CriticalStrip.Diagram.column_doubleSignTwist line 422
  42. lemma OAI.CriticalStrip.Diagram.signSpectral_deletionNode line 431
  43. lemma OAI.CriticalStrip.Diagram.signSpectral_deletionBeta line 436
  44. lemma OAI.CriticalStrip.Diagram.signSpectral_nodalScalar line 442
  45. lemma OAI.CriticalStrip.Diagram.signSpectral_nodalWeights line 457
  46. def OAI.CriticalStrip.Diagram.nodeSign line 489
  47. lemma OAI.CriticalStrip.Diagram.nodeSign_square line 492
  48. lemma OAI.CriticalStrip.Diagram.signSpectral_nodalVacuum line 499