Kostka Numbers

This Lean repository formalizes a key inequality from this paper of mine involving Kostka numbers. In order to prove the inequality, I defined Kostka numbers in Lean using their combinatorial definition as the number of semistandard Young tableau of a given shape and content. This repository also contains many properties of Kostka numbers that I needed for the result. Some highlights include the hook length formula and the fact that a Kostka number is positive iff its shape dominates its content.

At this time, I consider this project completed as I have fully formalized a proof of the inequality. I do intend to start upstream some lemmas to Mathlib and might eventually PR the definition of a Kostka number.

Structure

If you just want to verify the definitions and ensure the result I've formalize is an accurate translation of the mathematical statement into Lean, then look at Defs.lean and Inequality/Sum.lean. Most of the new definitions are in Defs and the statement of the main inequality is at the end of Sum (it is called kostka_inequality ).

Here is the organization of the project.

• Defs.lean contains the definition of Kostka numbers and the content of a SSYT as well as the definition of some special Young diagrams.
• Dominate.lean defines the dominance order on Lists and proves the results about it that I need.
• /Kostka establishes various results about Kostka numbers including values for particular shapes, a recursion, and the positivity result mentioned above.
• /Diagrams is primarily a collection of operations that produce new Young diagrams or new SSYT from old ones.
• /Computation includes the computation of some particular values of Kostka numbers and other results that are need for the technical case analysis of the proof.
• /HookLength is the proof of the hook length formula (more about that below).
• /Inequality brings all the pieces together. Each file proves a different case of the term by term inequality (Lemma 4.3 in the paper). Finally, Sum.lean proves the main inequality, kostka_inequality (Theorem 4.4 in the paper).
• /Util is a collection of basic lemmas (about Lists, Multisets, YoungDiagrams, and SemistandardYoungTableau). I intend to PR many of these to Mathlib.
• Other files not in a folder contain various lemmas or constructions that were used in the proof.

The Hook Length Formula

The hook length formula is proved in the /HookLength folder and roughly follows the probabilistic proof from Greene, Nijenhuis, and Wilf (1979). Mathlib doesn't have a lot of tools for making discrete probability arguments, so formalizing the experiment from GNW and getting the associated probability function is not currently possible. Instead, we define the notion of a hook path which represents the complete output of a trial in the experiment and define a probability function on those using a formula equivalent to the procedure given in GNW. This formula is a bit unwieldy to manipulate, so the proofs have some long calculations. As much as possible though, I did try to follow the spirit of the GNW proof and the arguments they presented. An algebraic proof of the hook length formula would likely be slicker, but Mathlib currently lacks the symmetric function theory needed for this.