OAI/RepresentationTheory/YoungSymmetry/Dimensions.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeShuffle.Specht.hilbertEquiv line 9

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:138 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:138 (same declaration text).

  2. def OAI.CubeShuffle.Specht.hilbertSpace line 13

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:142 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:142 (same declaration text).

  3. lemma OAI.CubeShuffle.Specht.finrank_hilbertSpace line 16
  4. lemma OAI.CubeShuffle.Specht.hilbert_action line 20
  5. lemma OAI.CubeShuffle.Specht.hilbertSpace_invariant line 26
  6. lemma OAI.CubeShuffle.Specht.tabloidAct_transitive line 41
  7. lemma OAI.CubeShuffle.Specht.polytabloid_pairing line 51
  8. lemma OAI.CubeShuffle.Specht.polytabloid_norm_sq line 63
  9. theorem OAI.CubeShuffle.Specht.dimension_times_column_ge_tabloids line 73

    Source documentation

    The genuine Specht dimension bound obtained from uncertainty in the transitive tabloid module; no hook formula or tableau spanning assumption.

    theorem dimension_times_column_ge_tabloids (μ : YoungDiagram) :
    Fintype.card (Tabloid μ) ≤ Module.finrank ℂ (space μ) * Fintype.card (colGroup μ) := by
…

    Mentions: OAI.CubeShuffle.Specht.Tabloid, OAI.CubeShuffle.Specht.space, OAI.CubeShuffle.Specht.colGroup

  10. def OAI.CubeShuffle.Specht.fiberGroupEquiv line 92
  11. lemma OAI.CubeShuffle.Specht.nat_card_fiberGroup line 119
  12. lemma OAI.CubeShuffle.Specht.card_fiberGroups_mul_le line 127

    Source documentation

    Row and column stabilizers of an injectively embedded finite incidence set have trivial intersection; their product embeds in the whole symmetric group.

    lemma card_fiberGroups_mul_le (f : α → β) (g : α → γ)
    (hinj : ∀ x y, f x = f y → g x = g y → x=y) :
    Fintype.card (fiberGroup f) * Fintype.card (fiberGroup g) ≤ (Fintype.card α).factorial := by
…

    Mentions: OAI.CubeShuffle.Specht.fiberGroup

  13. def OAI.CubeShuffle.Specht.rowGroup line 154
  14. def OAI.CubeShuffle.Specht.colIndex line 157
  15. lemma OAI.CubeShuffle.Specht.colGroup_eq line 160
  16. instance OAI.CubeShuffle.Specht.tabloidMulAction line 166
  17. lemma OAI.CubeShuffle.Specht.tabloid_orbit_all line 171
  18. lemma OAI.CubeShuffle.Specht.tabloid_stabilizer line 178
  19. lemma OAI.CubeShuffle.Specht.card_tabloid_mul_row line 191
  20. theorem OAI.CubeShuffle.Specht.factorial_le_dimension_row_column line 201

    Source documentation

    Fully algebraic factorial/product lower bound for the actual irreducible dimension.

    theorem factorial_le_dimension_row_column (μ : YoungDiagram) :
    μ.card.factorial ≤ Module.finrank ℂ (space μ)*Fintype.card (rowGroup μ)*Fintype.card (colGroup μ) := by
…

    Mentions: OAI.CubeShuffle.Specht.space, OAI.CubeShuffle.Specht.rowGroup, OAI.CubeShuffle.Specht.colGroup

  21. lemma OAI.CubeShuffle.Specht.card_row_fiber line 210
  22. lemma OAI.CubeShuffle.Specht.card_col_fiber line 216
  23. lemma OAI.CubeShuffle.Specht.card_rowGroup line 222
  24. lemma OAI.CubeShuffle.Specht.card_colGroup line 228
  25. abbrev OAI.CubeShuffle.Specht.Tail line 233
  26. lemma OAI.CubeShuffle.Specht.tail_card line 235
  27. lemma OAI.CubeShuffle.Specht.rowLen_zero_le_card line 240
  28. def OAI.CubeShuffle.Specht.tailColumnEquiv line 244
  29. lemma OAI.CubeShuffle.Specht.card_tail_col line 264
  30. lemma OAI.CubeShuffle.Specht.card_tail_row line 268
  31. lemma OAI.CubeShuffle.Specht.tail_row_group line 283
  32. lemma OAI.CubeShuffle.Specht.sum_tail_columns line 310
  33. lemma OAI.CubeShuffle.Specht.column_pos line 315
  34. lemma OAI.CubeShuffle.Specht.nat_le_two_pow_pred line 318
  35. lemma OAI.CubeShuffle.Specht.column_group_le_tail line 325
  36. theorem OAI.CubeShuffle.Specht.choose_tail_le_dimension line 343

    Source documentation

    Near-row dimension, preserving the actual polytabloid representation.

    theorem choose_tail_le_dimension (μ : YoungDiagram) :
    μ.card.choose (μ.card-μ.rowLen 0) ≤ Module.finrank ℂ (space μ) * 2^(μ.card-μ.rowLen 0) := by
…

    Mentions: OAI.CubeShuffle.Specht.space

  37. lemma OAI.CubeShuffle.Specht.exists_perm_mem_iff line 381
  38. def OAI.CubeShuffle.Specht.tailSet line 400
  39. lemma OAI.CubeShuffle.Specht.mem_tailSet line 403
  40. lemma OAI.CubeShuffle.Specht.tailSet_act line 406
  41. lemma OAI.CubeShuffle.Specht.card_tailSet line 414
  42. def OAI.CubeShuffle.Specht.footprint line 422
  43. lemma OAI.CubeShuffle.Specht.tail_fiber_card_eq line 425
  44. lemma OAI.CubeShuffle.Specht.footprint_card_product line 442
  45. lemma OAI.CubeShuffle.Specht.footprint_fixed line 474
  46. def OAI.CubeShuffle.Specht.fixedHilbert line 493
  47. lemma OAI.CubeShuffle.Specht.fixedHilbert_le line 503
  48. theorem OAI.CubeShuffle.Specht.fixedHilbert_dimension line 508

    Source documentation

    The quantitative near-row multiplicity bound from a genuine fixed coordinate footprint. This replaces, rather than assumes, the branching rule.

    theorem fixedHilbert_dimension (μ : YoungDiagram) (A : Finset (Cell μ)) :
    Module.finrank ℂ (space μ) * A.card.choose (μ.card-μ.rowLen 0) ≤
      Module.finrank ℂ (fixedHilbert μ A) * μ.card.choose (μ.card-μ.rowLen 0) := by
…

    Mentions: OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.space, OAI.CubeShuffle.Specht.fixedHilbert