OAI/RepresentationTheory/YoungSymmetry/UnitaryModel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeShuffle.Specht.spaceHilbertEquiv line 10

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

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

    Distinct definitions of this name: ComparatorChallenges/OccupiedOverlap.lean:148 (same statement text; different proof or body), ComparatorChallenges/WeightedSweepMoments.lean:148 (same statement text; different proof or body). Qualify references as OAI.CubeShuffle.Specht.unitaryRepresentation@path.

  3. lemma OAI.CubeShuffle.Specht.unitaryRepresentation_coe line 17
  4. def OAI.CubeShuffle.Specht.unitaryEquiv line 25
  5. lemma OAI.CubeShuffle.Specht.unitaryRepresentation_irreducible line 35
  6. lemma OAI.CubeShuffle.Specht.unitaryRepresentation_unitary line 40
  7. def OAI.CubeShuffle.Specht.tupleFixedEquiv line 52
  8. theorem OAI.CubeShuffle.Specht.tupleFixed_dimension line 71

    Source documentation

    True near-row multiplicity lower bound in the actual ordered-tuple action.

    theorem tupleFixed_dimension (μ : YoungDiagram) {ι : Type*} [Fintype ι]
    (e : ι ↪ Cell μ) :
    Module.finrank ℂ (hilbertSpace μ) * (Fintype.card ι).choose (μ.card-μ.rowLen 0) ≤
      Module.finrank ℂ (UnitaryFinite.fixedSpace (V := hilbertSpace μ) UnitaryFinite.tupleAction e (unitaryRepresentation μ)) *
…

    Mentions: OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.hilbertSpace, OAI.CubeShuffle.UnitaryFinite.fixedSpace, OAI.CubeShuffle.UnitaryFinite.tupleAction

  9. def OAI.CubeShuffle.Specht.relabelledUnitary line 87

    Distinct definitions of this name: ComparatorChallenges/OccupiedOverlap.lean:154 (same statement text; different proof or body), ComparatorChallenges/WeightedSweepMoments.lean:154 (same statement text; different proof or body). Qualify references as OAI.CubeShuffle.Specht.relabelledUnitary@path.

  10. lemma OAI.CubeShuffle.Specht.relabelledUnitary_unitary line 92
  11. lemma OAI.CubeShuffle.Specht.relabelledUnitary_irreducible line 98
  12. def OAI.CubeShuffle.Specht.relabelledTupleFixed line 103
  13. lemma OAI.CubeShuffle.Specht.relabelled_tuple_dimension line 137