OAI/RepresentationTheory/YoungSymmetry/ShapeBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CubeShuffle.Specht.choose_tail_le_of_factorial line 10

   Source documentation

   Tail bound for any genuine factorial row-column lower bound.

   theorem choose_tail_le_of_factorial (μ : YoungDiagram) (D : ℕ)
       (hd : μ.card.factorial ≤ D * Fintype.card (rowGroup μ) * Fintype.card (colGroup μ)) :
       μ.card.choose (μ.card-μ.rowLen 0) ≤ D * 2^(μ.card-μ.rowLen 0) := by
   …

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

2. lemma OAI.CubeShuffle.Specht.card_rowGroup_transpose line 44
3. lemma OAI.CubeShuffle.Specht.card_colGroup_transpose line 52
4. lemma OAI.CubeShuffle.Specht.card_transpose line 60
5. theorem OAI.CubeShuffle.Specht.choose_column_tail_le_dimension line 65

   Source documentation

   Near-column dimension without assuming transpose invariance of Specht dimensions.

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

   Mentions: OAI.CubeShuffle.Specht.space

6. lemma OAI.CubeShuffle.Specht.dimension_log_incidence line 78
7. lemma OAI.CubeShuffle.Specht.medium_dimension_raw line 101

   Source documentation

   Uniform dimension dichotomy. The proof only uses the proved factorial incidence bound and the proved tail binomial bound, not a tableau-count axiom.

   lemma medium_dimension_raw (μ : YoungDiagram) (hμ : 0<μ.card) (δ : ℝ) (hδ : 0<δ)
       (hδ2 : δ≤1/2) (hrow : δ*(μ.card:ℝ)≤μ.card-μ.rowLen 0)
       (hcol : (μ.colLen 0:ℝ)≤(μ.card:ℝ)/2) :
       min ((3/2:ℝ)*Real.log 2-1) (entropyGap*δ)*(μ.card:ℝ)-2*Real.log μ.card-1≤
         Real.log (Module.finrank ℂ (space μ)) := by
   …

   Mentions: OAI.CubeShuffle.Specht.space

8. theorem OAI.CubeShuffle.Specht.medium_dimension line 157

   Source documentation

   Genuine uniform exponential dimension growth off the near-row regime; tall columns are handled by the separate, exactly proved killing theorem.

   theorem medium_dimension (δ : ℝ) (hδ : 0<δ) (hδ2 : δ≤1/2) :
       ∃ h : ℝ, 0<h ∧ ∀ᶠ N : ℕ in atTop, ∀ μ : YoungDiagram, μ.card=N →
         δ*(N:ℝ)≤N-μ.rowLen 0 → (μ.colLen 0:ℝ)≤(N:ℝ)/2 →
         h*(N:ℝ)≤Real.log (Module.finrank ℂ (space μ)) := by
   …

   Mentions: OAI.CubeShuffle.Specht.space

9. lemma OAI.CubeShuffle.Specht.partition_count line 180
10. lemma OAI.CubeShuffle.Specht.shapes_count line 185
11. lemma OAI.CubeShuffle.Specht.rowLens_headD line 189
12. lemma OAI.CubeShuffle.Specht.rowLens_tail_sum line 201
13. lemma OAI.CubeShuffle.Specht.positive_list_eq_of_tail_sum line 212
14. abbrev OAI.CubeShuffle.Specht.TailShapes line 239
15. def OAI.CubeShuffle.Specht.tailShapePartition line 241
16. lemma OAI.CubeShuffle.Specht.tailShapePartition_injective line 246
17. lemma OAI.CubeShuffle.Specht.tail_shapes_count line 262