OAI/RepresentationTheory/Young/Entropy.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoordinateSweeps.YoungCorner.sumRow line 13
2. def OAI.CoordinateSweeps.YoungCorner.sumCol line 16
3. lemma OAI.CoordinateSweeps.YoungCorner.sumRow_right line 20
4. lemma OAI.CoordinateSweeps.YoungCorner.sumCol_left line 26
5. lemma OAI.CoordinateSweeps.YoungCorner.swap_mem_rows line 41
6. lemma OAI.CoordinateSweeps.YoungCorner.swap_mem_cols line 50
7. lemma OAI.CoordinateSweeps.YoungCorner.corner_zero_of_collision line 60

   Source comment

   Transposition cancellation in a Young row/column corner.

   lemma corner_zero_of_collision (μ : YoungDiagram) (ρ : Equiv.Perm (Boxes μ) →* A)
       (σ : Equiv.Perm (Boxes μ)) (x y : Boxes μ) (hxy : x ≠ y)
       (hrow : x.val.1=y.val.1) (hcol : (σ⁻¹ x).val.2=(σ⁻¹ y).val.2) :
       sumRow μ ρ * ρ σ * sumCol μ ρ=0 := by
   …

   Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.sumRow, OAI.CoordinateSweeps.YoungCorner.sumCol

8. theorem OAI.CoordinateSweeps.YoungCorner.corner_scalar line 98

   Source comment

   The one-dimensional Young corner in every complex matrix representation, proved by Ferrers sorting.

   theorem corner_scalar (μ : YoungDiagram) (ρ : Equiv.Perm (Boxes μ) →* A)
       (σ : Equiv.Perm (Boxes μ)) :
       ∃ c : ℂ, sumRow μ ρ * ρ σ * sumCol μ ρ = c • (sumRow μ ρ * sumCol μ ρ) := by
   …

   Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.YoungCorner.sumRow, OAI.CoordinateSweeps.YoungCorner.sumCol

9. def OAI.CoordinateSweeps.RepDetection.orbitSpan line 117
10. lemma OAI.CoordinateSweeps.RepDetection.mem_orbitSpan line 130
11. lemma OAI.CoordinateSweeps.RepDetection.orbitSpan_le line 134
12. def OAI.CoordinateSweeps.YoungCorner.unitVector line 144
13. def OAI.CoordinateSweeps.YoungCorner.columnGenerator line 146
14. def OAI.CoordinateSweeps.YoungCorner.youngVector line 147
15. abbrev OAI.CoordinateSweeps.YoungCorner.columnModule line 148
16. lemma OAI.CoordinateSweeps.YoungCorner.youngVector_one line 150
17. lemma OAI.CoordinateSweeps.YoungCorner.youngVector_ne_zero line 159
18. lemma OAI.CoordinateSweeps.YoungCorner.youngVector_mem line 165
19. lemma OAI.CoordinateSweeps.YoungCorner.sumRow_square line 172
20. lemma OAI.CoordinateSweeps.YoungCorner.sumRow_youngVector line 180
21. lemma OAI.CoordinateSweeps.YoungCorner.rowImage_line line 187
22. lemma OAI.CoordinateSweeps.YoungCorner.col_row_col_eq_one line 210
23. lemma OAI.CoordinateSweeps.YoungCorner.col_youngVector_one line 223
24. lemma OAI.CoordinateSweeps.YoungCorner.col_youngVector_ne_zero line 234
25. lemma OAI.CoordinateSweeps.YoungCorner.spechtSeed_exists line 246
26. lemma OAI.CoordinateSweeps.YoungCorner.rank_row_col line 320

    Source comment

    A rank-preserving row-times-column factor has to be the identity. This gives independent Young vectors for the entire rank stabilizer.

    lemma rank_row_col (μ : YoungDiagram) (r : rows μ) (c : cols μ)
        (h : ∀ x : Boxes μ, ((r.val*c.val) x).val.1+((r.val*c.val) x).val.2=x.val.1+x.val.2) :
        r=1 ∧ c=1 := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.rows, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.YoungCorner.cols, OAI.CoordinateSweeps.YoungCorner.Boxes

27. lemma OAI.CoordinateSweeps.YoungCorner.card_perm_le_colors_mul_stabilizer line 386
28. def OAI.CoordinateSweeps.YoungCorner.ranks line 412
29. lemma OAI.CoordinateSweeps.YoungCorner.youngVector_rank_value line 415
30. lemma OAI.CoordinateSweeps.YoungCorner.rankVectors_eval line 434
31. lemma OAI.CoordinateSweeps.YoungCorner.rankVectors_independent line 440
32. lemma OAI.CoordinateSweeps.YoungCorner.rank_card_le_shape_finrank line 448
33. lemma OAI.CoordinateSweeps.YoungCorner.shape_dimension_entropy line 473

    Source comment

    Entropy lower bound from Young vectors for the removed-diagram step of the main induction.

    lemma shape_dimension_entropy (μ : YoungDiagram) {V : Type} [AddCommGroup V]
        [Module ℂ V] [FiniteDimensional ℂ V] (τ : Representation ℂ (Equiv.Perm (Boxes μ)) V)
        [τ.IsIrreducible] (hτ : hasShape μ (Equiv.refl _) τ)
        (L : ℕ) (hL : ∀ x : Boxes μ, x.val.1+x.val.2<L) :
        (Fintype.card (Boxes μ)).factorial ≤ L^(Fintype.card (Boxes μ))*Module.finrank ℂ V := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.hasShape