OAI/RepresentationTheory/Saxl/PathContraction.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Saxl.Path.Mat line 10
2. abbrev OAI.Saxl.Path.Letter line 11
3. def OAI.Saxl.Path.parts line 13
4. def OAI.Saxl.Path.J line 14
5. def OAI.Saxl.Path.leftPos line 16
6. def OAI.Saxl.Path.midPos line 17
7. def OAI.Saxl.Path.rightPos line 18
8. def OAI.Saxl.Path.bandWord line 22

   Source comment

   EXACT coefficients of the path-ordered alternating band: the two endpoint singletons carry letter 0, and row/column pairs have coefficients J. Here r=m-1.

   def bandWord (r : ℕ) (w : Fin (2 * r + 1) → Letter) : ℂ :=
   …

   Mentions: OAI.Saxl.Path.Letter

9. def OAI.Saxl.Path.pureWord line 29

   Source comment

   Ordinary pure position tensor pairing, with no conjugation.

   def pureWord {n : ℕ} (X : Fin n → Mat) (w : Fin n → Letter) : ℂ :=
   …

   Mentions: OAI.Saxl.Path.Mat, OAI.Saxl.Path.Letter

10. def OAI.Saxl.Path.entry line 32
11. def OAI.Saxl.Path.DL line 34
12. def OAI.Saxl.Path.chainML line 47
13. lemma OAI.Saxl.Path.chainML_apply line 50
14. lemma OAI.Saxl.Path.entry_sum line 53
15. lemma OAI.Saxl.Path.chain_expand line 59
16. lemma OAI.Saxl.Path.adj_entry line 73
17. lemma OAI.Saxl.Path.D_shift line 78
18. lemma OAI.Saxl.Path.chain_step line 81
19. lemma OAI.Saxl.Path.pair_product_step line 98
20. lemma OAI.Saxl.Path.chain_entries line 108
21. lemma OAI.Saxl.Path.chain_entries_endpoint line 133
22. theorem OAI.Saxl.Path.path_contraction line 141
23. lemma OAI.Saxl.Path.J_real line 161
24. lemma OAI.Saxl.Path.bandWord_real line 164