Young diagram helpers

Shared Young-diagram vocabulary: the square diagram and the hook membership predicate. The hook IsInHook a b μ is the confinement region of the alive shapes in the hook-confinement argument, and the square diagram is the shape whose dimension growth drives that confinement.

def RS.squareDiagram (s : ℕ) : YoungDiagram

The s × s square Young diagram.

Equations

• RS.squareDiagram s = YoungDiagram.ofRowLens (List.replicate s s) ⋯

def RS.IsInHook (a b : ℕ) (μ : YoungDiagram) : Prop

Membership in the (a, b) hook: every row after the first a has length at most b (rows are indexed from 0, so this reads rowLen a ≤ b by antitonicity of row lengths).

Equations

• RS.IsInHook a b μ = (μ.rowLen a ≤ b)

Square diagram: row lengths and membership

theorem RS.squareDiagram_rowLens (s : ℕ) : (squareDiagram s).rowLens = List.replicate s s

The row-length list of the s × s square diagram is s copies of s.

@[simp]

theorem RS.mem_squareDiagram {s : ℕ} {c : ℕ × ℕ} : c ∈ squareDiagram s ↔ c.1 < s ∧ c.2 < s

A cell (i, j) lies in the s × s square diagram precisely when both coordinates are strictly below s.

theorem RS.rowLen_squareDiagram {s a : ℕ} (ha : a < s) : (squareDiagram s).rowLen a = s

The length of row a in the s × s square diagram is s when a < s.

theorem RS.squareDiagram_card (s : ℕ) : (squareDiagram s).card = s ^ 2

The cardinality (number of cells) of the s × s square diagram is s².

Square diagram containment

theorem RS.squareDiagram_le_of_rowLen {s : ℕ} {μ : YoungDiagram} (h : s ≤ μ.rowLen (s - 1)) : squareDiagram s ≤ μ

If the (s − 1)-th row of μ has length at least s, the s × s square fits inside μ.

Hook predicate

theorem RS.not_isInHook_iff {a b : ℕ} {μ : YoungDiagram} : ¬IsInHook a b μ ↔ b < μ.rowLen a

The negation of the hook predicate is equivalent to the cell (a, b) belonging to the diagram.

List-to-diagram bridge

theorem RS.rowLen_ofRowLens_getD {w : List ℕ} {hw : w.SortedGE} (i : ℕ) : (YoungDiagram.ofRowLens w hw).rowLen i = w.getD i 0

The row length of the diagram built from w at index i equals w.getD i 0: the i-th entry when i is in range, and 0 otherwise.

theorem RS.YoungDiagram.card_le_card {lam mu : YoungDiagram} (hle : lam ≤ mu) : lam.card ≤ mu.card

Containment of diagrams is containment of cell sets, so the cell count is monotone.

theorem RS.card_eq_sum_rowLens (μ : YoungDiagram) : μ.card = μ.rowLens.sum

The number of cells of a Young diagram is the sum of its row lengths.