OAI/RepresentationTheory/Saxl/BandMatrices.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Saxl.Band.Mat line 12
2. def OAI.Saxl.Band.basis line 14
3. def OAI.Saxl.Band.D line 21
4. def OAI.Saxl.Band.segment line 23
5. def OAI.Saxl.Band.blocks line 29

   Source comment

   Consecutive segments with the original global position parities.

   def blocks : ℕ → List ℕ → Mat
     | _, [] => 1
     | p, r :: rs => segment r p * blocks (p + r) rs
   
   /- Enumeration of the finite symmetric group for the four small matrix calculations. -/

   Mentions: OAI.Saxl.Band.Mat, OAI.Saxl.Band.segment

6. lemma OAI.Saxl.Band.sum_perm_succ line 34

   Source comment

   Enumeration of the finite symmetric group for the four small matrix calculations.

   lemma sum_perm_succ {A : Type uA} [AddCommMonoid A] (n : ℕ)
       (f : Equiv.Perm (Fin (n + 1)) → A) :
       (∑ π, f π) = ∑ i : Fin (n + 1), ∑ σ : Equiv.Perm (Fin n),
         f (Equiv.Perm.decomposeFin.symm (i, σ)) := by
   …

7. lemma OAI.Saxl.Band.decompose_apply_two line 44
8. lemma OAI.Saxl.Band.decompose_apply_three line 49
9. lemma OAI.Saxl.Band.segment_one_even line 54
10. lemma OAI.Saxl.Band.segment_one_odd line 57
11. lemma OAI.Saxl.Band.segment_two_even line 60
12. lemma OAI.Saxl.Band.segment_two_odd line 78
13. lemma OAI.Saxl.Band.segment_three_even line 96
14. lemma OAI.Saxl.Band.segment_three_odd line 114
15. lemma OAI.Saxl.Band.segment_four_even line 132
16. lemma OAI.Saxl.Band.segment_four_odd line 150
17. lemma OAI.Saxl.Band.segment_mod line 169

    Source comment

    Only the original global parity matters.

    lemma segment_mod (r p : ℕ) : segment r p = segment r (p % 2) := by
    …

    Mentions: OAI.Saxl.Band.segment

18. def OAI.Saxl.Band.ScaledBasis line 172
19. lemma OAI.Saxl.Band.scaledBasis_smul line 175
20. lemma OAI.Saxl.Band.scaledBasis_one line 178
21. lemma OAI.Saxl.Band.basis_mul line 181
22. lemma OAI.Saxl.Band.ScaledBasis.mul line 248
23. lemma OAI.Saxl.Band.segment_scaled line 256
24. lemma OAI.Saxl.Band.blocks_scaled line 270
25. def OAI.Saxl.Band.Q line 278
26. def OAI.Saxl.Band.Qinv line 279
27. lemma OAI.Saxl.Band.Q_mul_Qinv line 281
28. lemma OAI.Saxl.Band.Qinv_mul_Q line 286
29. lemma OAI.Saxl.Band.Q_isUnit line 291
30. lemma OAI.Saxl.Band.Q_inverse line 293
31. lemma OAI.Saxl.Band.Q_basis_ne_zero line 296
32. theorem OAI.Saxl.Band.band_nonzero_pairing line 301

    Source comment

    Endpoint noncancellation for arbitrary consecutive columns of lengths at most four.

    theorem band_nonzero_pairing (rs : List ℕ)
        (hrs : ∀ r ∈ rs, 1 ≤ r ∧ r ≤ 4) :
        ∃ Q : Mat, IsUnit Q ∧ (Q * blocks 1 rs * Q⁻¹) 0 0 ≠ 0 := by
    …

    Mentions: OAI.Saxl.Band.Q, OAI.Saxl.Band.Mat, OAI.Saxl.Band.blocks