OAI/Combinatorics/StripMass/NorthMerging.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.polynomialNorthSource_merge line 12
  2. theorem OAI.CriticalStrip.Diagram.polynomialNorthSource_delete line 62
  3. def OAI.CriticalStrip.Diagram.reflectionMonomial line 127
  4. def OAI.CriticalStrip.Diagram.reflectLaurent line 136
  5. lemma OAI.CriticalStrip.Diagram.reflectLaurent_monomial line 139
  6. lemma OAI.CriticalStrip.Diagram.reflectLaurent_involutive line 147
  7. def OAI.CriticalStrip.Diagram.reflectSpectral line 157
  8. lemma OAI.CriticalStrip.Diagram.reflectSpectral_evalLaurent line 163
  9. lemma OAI.CriticalStrip.Diagram.reflectSpectral_involutive line 167
  10. lemma OAI.CriticalStrip.Diagram.reflectSpectral_const line 176
  11. lemma OAI.CriticalStrip.Diagram.reflectSpectral_variable line 184
  12. lemma OAI.CriticalStrip.Diagram.reflectSpectral_torusSin line 194
  13. lemma OAI.CriticalStrip.Diagram.reflectSpectral_torusCos line 198
  14. lemma OAI.CriticalStrip.Diagram.reflectSpectral_torusL line 202
  15. lemma OAI.CriticalStrip.Diagram.reflectSpectral_torusWeights line 205
  16. lemma OAI.CriticalStrip.Diagram.reflectSpectral_spectralA line 209
  17. lemma OAI.CriticalStrip.Diagram.reflectSpectral_normalization line 217
  18. lemma OAI.CriticalStrip.Diagram.reflectLaurent_perm line 222
  19. lemma OAI.CriticalStrip.Diagram.reflectSpectral_perm line 235
  20. lemma OAI.CriticalStrip.Diagram.reflectLaurent_sign line 246
  21. lemma OAI.CriticalStrip.Diagram.reflectSpectral_sign line 258
  22. lemma OAI.CriticalStrip.Diagram.LaurentBox.reflect line 269
  23. lemma OAI.CriticalStrip.Diagram.sourceBlock_map line 288
  24. lemma OAI.CriticalStrip.Diagram.sourceBlock_transpose line 292
  25. lemma OAI.CriticalStrip.Diagram.LastMatrix.source_mul line 296
  26. lemma OAI.CriticalStrip.Diagram.glueMatrix_last line 303
  27. lemma OAI.CriticalStrip.Diagram.LastMatrix.transpose line 310
  28. def OAI.CriticalStrip.Diagram.sourceGlue line 317
  29. lemma OAI.CriticalStrip.Diagram.sourceGlue_symmetric line 321
  30. lemma OAI.CriticalStrip.Diagram.sourceGlue_map line 328
  31. lemma OAI.CriticalStrip.Diagram.sourceGlue_adjoint line 334
  32. lemma OAI.CriticalStrip.Diagram.polynomialNorthSource_eval_numerator line 357
  33. lemma OAI.CriticalStrip.Diagram.polynomialNorthSource_covariance line 364
  34. lemma OAI.CriticalStrip.Diagram.polynomialNorthSource_parity line 376
  35. lemma OAI.CriticalStrip.Diagram.permSpectral_swap_involutive line 383
  36. def OAI.CriticalStrip.Diagram.polynomialNorthGluing line 402
  37. lemma OAI.CriticalStrip.Diagram.sourceGlue_eq_sum line 406