OAI/Combinatorics/StripMass/SplitProjection.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.Pairing.mapRestrict_eq_of_supported line 15
  2. lemma OAI.CriticalStrip.Diagram.Pairing.mapRestrict_omit line 28
  3. lemma OAI.CriticalStrip.Diagram.Pairing.join_map line 36
  4. lemma OAI.CriticalStrip.Diagram.Pairing.join_map_reach line 47
  5. lemma OAI.CriticalStrip.Diagram.Pairing.gluesAt_map line 69
  6. lemma OAI.CriticalStrip.Diagram.Pairing.gluesAt_map_supported line 93
  7. theorem OAI.CriticalStrip.Diagram.functionMatrix_glue_adjoint line 106
  8. lemma OAI.CriticalStrip.Diagram.functionMatrix_transpose_mul_self line 123
  9. lemma OAI.CriticalStrip.Diagram.localR_vacant_right line 132
  10. def OAI.CriticalStrip.Diagram.splitProjection line 170
  11. theorem OAI.CriticalStrip.Diagram.splitProjection_glue_adjoint line 175
  12. lemma OAI.CriticalStrip.Diagram.transpose_functionMatrix_mul_apply line 195
  13. lemma OAI.CriticalStrip.Diagram.vacant_restriction_localR line 201
  14. lemma OAI.CriticalStrip.Diagram.vacant_restriction_localR_mulVec line 211
  15. theorem OAI.CriticalStrip.Diagram.splitMap_injective line 225
  16. lemma OAI.CriticalStrip.Diagram.mergeMap_injective line 237
  17. lemma OAI.CriticalStrip.Diagram.sum_tiles line 248
  18. lemma OAI.CriticalStrip.Diagram.mul_localR_apply line 255
  19. lemma OAI.CriticalStrip.Diagram.localR_apply line 263
  20. lemma OAI.CriticalStrip.Diagram.Pairing.mapOccupied_equiv_occupied line 276
  21. lemma OAI.CriticalStrip.Diagram.Pairing.moveIntoVacancy_occupied line 286
  22. lemma OAI.CriticalStrip.Diagram.Pairing.moveIntoLowerVacancy_occupied line 291
  23. lemma OAI.CriticalStrip.Diagram.Pairing.insertCup_occupied line 296
  24. lemma OAI.CriticalStrip.Diagram.Pairing.moveIntoLowerVacancy_inverse line 301
  25. def OAI.CriticalStrip.Diagram.vacantProjection line 312
  26. lemma OAI.CriticalStrip.Diagram.mul_vacantProjection_apply line 315
  27. lemma OAI.CriticalStrip.Diagram.functionMatrix_mul_transpose_omit line 321
  28. theorem OAI.CriticalStrip.Diagram.localR_factor_merge line 353
  29. lemma OAI.CriticalStrip.Diagram.sin_lambda_eq_c line 417
  30. lemma OAI.CriticalStrip.Diagram.sin_three_lambda_eq_C line 423
  31. lemma OAI.CriticalStrip.Diagram.sin_four_lambda_eq_one line 429
  32. lemma OAI.CriticalStrip.Diagram.C_ne_zero line 432
  33. lemma OAI.CriticalStrip.Diagram.d_mul_c_div_C line 436
  34. lemma OAI.CriticalStrip.Diagram.d_sq_div_C line 444
  35. lemma OAI.CriticalStrip.Diagram.torusL_phase_two line 448
  36. lemma OAI.CriticalStrip.Diagram.torusWeights_phase_two line 457
  37. def OAI.CriticalStrip.Diagram.mergeProjection line 482
  38. theorem OAI.CriticalStrip.Diagram.mergeMap_mul_projection line 489
  39. lemma OAI.CriticalStrip.Diagram.functionMatrix_vacantProjection line 513
  40. def OAI.CriticalStrip.Diagram.twoVacancyInsertion line 526
  41. lemma OAI.CriticalStrip.Diagram.twoVacancyInsertion_mul_transpose line 531
  42. lemma OAI.CriticalStrip.Diagram.localR_factor_deletion line 563
  43. def OAI.CriticalStrip.Diagram.deletionProjection line 605
  44. theorem OAI.CriticalStrip.Diagram.deletionMap_mul_projection line 610