Library Combi.Combi.bintree: Binary Trees

• Binary Trees
• Inductive type for binary trees
  • Catalan numbers
  • Left branch surgery in binary trees
  • Various particular binary trees
• Tamari's lattice
  • Rotations in binary trees
  • Tamari vectors
  • Bijection with Tamari vectors
  • Comparison of Tamari vectors
• Correspondence between rotation on binary trees and Tamari vectors
  • Definition of Tamari order

Library Combi.Combi.composition: Integer Composition

• Integer Compositions.
  • Definitions and basic properties
• Sigma Types for Compositions
• Bijection with subsets

Library Combi.Combi.Dyckword: Dyck Words

• Dyck Words
• Braces and Dyck words
  • Height of a word
  • Definitions
  • Sigma type for Dyck words
• Standard factorization of Dyck words
  • Induction on Dyck words following the standard factorization
  • Examples of application of the induction principle
  • Bijection with binary trees
• Dyck and balanced words
  • Rotation map from balanced words to a Dyck words
• Catalan numbers
  • The rotation bijection
  • Main theorem for catalan numbers

Library Combi.Combi.fibered_set: Bijection beetween fibered sets

• Bijection beetween fibered sets

Library Combi.Combi.partition: Integer Partitions

• Shapes and Integer Partitions
• Shapes
• Integer Partitions
  • Definitions and basic properties
  • Corners, adding and removing corners
  • Conjugate of a partition
  • Partial sum of partitions
• Inclusion of Partitions and Skew Partitions
• Sigma Types for Partitions
  • Hook shaped partitions
  • Removing a corner from a partition
  • Lexicographic order on partitions of a fixed sum
• Counting functions
• A finite type finType for coordinate of boxes inside a shape
  • Rewriting bigops running along the boxes of a shape
  • Adding a box to a shape
• The union of two integer partitions
• Young lattice on partition
• Dominance order on partition
• Shape of set partitions and integer partitions

Library Combi.Combi.permuted: Listing the Permutations of a tuple or seq

• The list of the permuted tuple of a given tuple
  • Enumeration of the permutation of a tuple
  • Permutation of a tuple as a fintype
• Action of 'S_n on permuted for and n.-tuple T.
  • The stabilizer of a tuple under permutation

Library Combi.Combi.multinomial: Multinomial Coefficients

• Multinomial Coefficients

Library Combi.Combi.setpartition: Set Partitions

• Set Partitions and refinment lattice

Library Combi.Combi.skewpart: Skew Partitions

• Skew partitions:
• Horizontal and vertical border strips
• Ribbon border strip
  • The first common drop of two sequences
  • An operative definition for ribbon border strips
  • Equivalence with the textbook definition
    • Some complement on connect
    • 4 neigborhood
    • The textbook definition

Library Combi.Combi.skewtab: Skew Tableaux

• Skew tableau and skew yamanouchi words:
  • Skew Yamanouchi words
  • Skew tableaux
  • Skewing and joining tableaux
  • Standardisation of a tableau

Library Combi.Combi.std: Standard Words, i.e. Permutation as Words

• Standard words
• Standard words and permutations
• Standard words as a finType
• Standardisation of a word over a totally ordered alphabet
  • Inversion sets and standardization
  • Standardization and elementary transpositions of a word
• Inverse of a standard word
• inverse of the standardized of w

Library Combi.Combi.stdtab: Standard Tableaux

• Standard Tableaux
  • Appending on the n-th row
  • Finding the largest entry
• Bijection standard tableau <-> Yamanouchi words
• Sigma type for standard tableaux
• Conjugate of a standard tableau

Library Combi.Combi.subseq: Subsequence of a sequence as a fintype

• Subsequence of a sequence as a fintype
  • A few lemmas about subseq and rcons
• Subsequence of a sequence as a fintype
• Relating sub sequences of iota and being sorted

Library Combi.Combi.tableau: Young Tableaux

• Young Tableaux over an ordtype
  • Specialization of sorted Lemmas
  • Dominance order for rows
• Tableaux : definition and basic properties
  • Cuting rows and tableaux
  • The size of a tableau
  • Tableaux from their row reading
  • Sigma type for tableaux
  • Tableaux and increasing maps

Library Combi.Combi.vectNK: Integer Vector of Given Sums and Sizes

• Integer vectors of sum n and size k

Library Combi.Combi.Yamanouchi: Yamanouchi Words

• Yamanouchi words.
• Evaluation of a sequence of integer (mostly Yamanouchi word)
• Yamanouchi words:
  • Hyperstandard Yamanouchi word : 33 2222 11111 0000000
• Enumeration of Yamanouchi words
• Sigma types for Yamanouchi words

Library Combi.Erdos_Szekeres.Erdos_Szekeres: The Erdös-Szekeres theorem

• The Erdös-Szekeres theorem on monotonic subsequences.

Library Combi.LRrule.extract: Extracting the implementation to OCaml

• A certified OCaml implementation
  • The Littlewood-Richardson Rule

Library Combi.LRrule.freeSchur: Free Schur functions

• Free Schur functions
• Commutative image of an homogeneous langage
  • Row reading of tableau
• Free Schur function : lifting Schur function is the free algebra
  • Noncommutative lifting of Schur polynomials
  • Commutative image of freeSchur language
• The free Littlewood-Richardson rule
  • Invariance with respect to choice of the Q-Tableau
  • Conjugating tableaux in the free LR rule

Library Combi.LRrule.Greene: Greene monotone subsequence numbers

• Greene monotone subsequences numbers
  • Trivial intersection sequences
• Greene subsequence numbers
  • Definition and basic properties
  • Greene numbers of a concatenation
  • Injection of k-supports
  • Reverting a word on the dual alphabet
• Greene number for tableaux
  • Induction step: adding a row to a tableau
  • Greene numbers of a tableau
  • Recovering a shape from Greene numbers on tableaux

Library Combi.LRrule.Greene_inv: Greene subsequence theorem

• Greene subsequence theorem
  • k-Support and order duality
• Swaping two letters in a word and its k-supports
  • Case where no sets contains both
  • Cover surgery
  • Case where a set in P contains both a and c
    • Generic order hypothesis
    • Case where b is not in cover P
    • Case where b is in cover P
    • Existence theorem for k-supports
• Greene numbers are invariant by each plactic rules
  • Deducing the other comparisons by duality
  • Invariance by the rules
• Main theorem
  • Row Greene number
  • Column Greene number
  • Robinson-Schensted and the plactic monoid
  • Reverting uniq words

Library Combi.LRrule.implem: A Coq implementation of the Littlewood-Richarson rule

• A Coq implementation of the Littlewood-Richarson rule
• Recursive enumeration and counting function
  • LRyamtab_list_rec returns only Yamanouchi words
  • LRyamtab_list_rec returns words whose evaluation in included in outev
  • LRyamtab_list_rec returns fillings of skew shape inner/outer
  • LRyamtab_list_rec returns legitimate skew_tableaux
  • Mutiplicities are all one
• The main functions
• The specification of the enumeration function
  • The specification on sigma types
• Back to the rule

Library Combi.LRrule.plactic: The plactic monoid

• The plactic monoid
• Definition of the Plactic monoid
  • Plactic equivalence and reversal
  • Plactic equivalence and order duality
• Plactic monoid and Robinson-Schensted map
  • Removing the last big letter and plactic congruence
  • Plactic congruence and increasing maps

Library Combi.LRrule.Schensted: The Robinson-Schensted correspondence

• The Robinson-Schensted correspondence
• Schensted's algorithm
  • Row insertion
  • The algorithm
  • Schensted's algorithem specifications
• Robinson-Schensted bumping
  • bumping a letter
  • The insertion tableau
  • Inverting a bump
  • The Robinson-Schensted insertion with recording
  • Invertion a Robinson-Schensted step
• Robinson-Schensted correspondence
  • The Robinson-Schensted map
  • The inverse Robinson-Schensted inverse map
  • Statistics preserved by the Robinson-Schensted map
  • Sigma types and bijections
  • Robinson-Schensted classes
• The Robinson-Schensted map with standard recording tableau

Library Combi.LRrule.shuffle: Shuffle and shifted shuffle

• Shuffle, shifted shuffle and plactic classes
  • The shuffle of two sequences
    • Shuffling two disjoint sequences
  • The shifted shuffle of two standard words
  • Schützenberger theorem
• Shifted shuffle and inverse standardized
• Littlewood-Richardson-Schützenberger triple
  • A longer alternative road
  • Conjugating LRtriple

Library Combi.LRrule.stdplact: Plactic congruences and standardization

• Plactic congruences and standardization
  • Plactic congruence and standardization
  • Robinson-Schensted correspondence and standardization
  • Robinson-Schensted correspondence and inversion

Library Combi.LRrule.therule: The Littlewood-Richardson rule

• The Littlewood-Richardson rule
• Gluing a standard tableaux with a skew tableau
• Littlewood-Richardson Yamanouchi tableaux
  • The final bijection
  • A slow way to compute LR coefficients in coq:
• The statement of the Littlewood-Richardson rule
• Pieri's rules

Library Combi.LRrule.Yam_plact: Plactic classes and Yamanouchi words

• Plactic classes and Yamanouchi words
• The Yamanouchi tableau
• Yamanouchi words, standardization and plactic classes

Library Combi.SSRcomplements.ordcast: Cast between ordinals

• Some complement on casts between ordinals

Library Combi.SSRcomplements.sorted: [path] and [sorted] complements

• Various Lemmas about path and sorted which are missing in MathComp

Library Combi.SSRcomplements.permcomp: Complement on permutations

• A few lemmas on permutation
  • Orbit and cycles

Library Combi.SSRcomplements.tools: Missing SSReflect sequence and set lemmas

• A bunch of lemmas about seqs and sets which are missing in SSReflect
  • rcons and cons related lemmas
  • set_nth related lemmas
  • minn related lemmas
  • sumn related lemmas
  • iota related lemmas

Library Combi.HookFormula.Frobenius_ident

• Combi.hook.Frobenius_ident : Frobenius identity
• A proof of Frobenius identity:

Library Combi.HookFormula.hook: A proof of the Hook-Lenght formula

• A proof of the Hook-Lenght formula
• Recursion for the number of Yamanouchi words and standard tableaux
• Boxes, Hooks and corners
  • Hook boxes
  • Traces
• The probabilistic algorithm
• The proof

Library Combi.Basic.combclass: Fintypes for Combinatorics

• Fintypes for Combinatorics
• Building subtype from a sequence
  • Method 2 - Each element appears and the lists is uniq
  • Method 3 - Each element appears, we remove the duplicates
• Finite subtype obtained as a finite the dijoint union of finite subtypes

Library Combi.Basic.congr: Rewriting rule and congruencies of words

• Equivalence and congruence closure of a rewriting rule on words
  • Transitive closure of a rule with finite classes
  • Dealing with the dependance of invar on x
  • Basic facts on congruences:
  • Congruence closure of a bounded rule
• Multi-homogeneous congruence rules
• Homogeneous congruence rules on a finite type

Library Combi.Basic.ordtype: Ordered Types

• Ordered type
• Induction on partially ordered types
• Covering relation
• Inhabited types
  • Inhabited ordered types
  • Inhabited finite partially ordered types
• sequences over an ordered types
  • • Maximum of a sequence
    • Comparison of the elements of a sequence to an element
    • Removing the largest letter of a sequence

Library Combi.Basic.unitriginv: Uni-triangular Matrices

• Triangular matrix with 1 on the diagonal

Library Combi.SymGroup.cycles: The Cycle Decomposition of a Permutation

• The Cycle Decomposition of a Permutation
  • Support of a permutation
  • porbit_set of a permutation
  • Cyclic permutations
• Decomposition of a permutation by restriction to disjoint stable subsets
  • Disjoint psupport and commutation
  • Cycle decomposition of a permutation

Library Combi.SymGroup.cycletype: The Cycle Type of a Permutation

• Cycle type and conjugacy classes in the symmetric groups
• Cycle maps
• Cycle type and conjugacy classes
• Cycle indicator
  • Central function for 'S_n

Library Combi.SymGroup.Frobenius_char: Frobenius characteristic

• Frobenius / Schur character theory for the symmetric groups.
• Definition and basic properties
  • Frobenius Characteristic and omega involution
  • The Frobenius Characteristic is an isometry
  • The Frobenius Characteristic is a graded ring morphism
• Combinatorics of characters of the symmetric groups
  • Young characters and Young Rule
  • Irreducible character
  • Frobenius character formula for 'SG_n
• Littlewood-Richardson rule for irreducible characters

Library Combi.SymGroup.permcent: The Centralizer of a Permutation

• The Centralizer of a Permutation
  • Support and cycle in the centralizer
  • The cyclic centralizer
  • Permuting the cycles among themselves
• Main theorem
  • Conjucacy class cardinality

Library Combi.SymGroup.presentSn: The Coxeter Presentation of the Symmetric Group

• The Coxeter Presentation of the Symmetric Group
• Codes for permutations
  • Fintype for codes for permutations of size n
• Elementary transpositions
• Inversion set of a permutation
• Length of a permutation
• The canonical reduced word of a permutation
  • Properties of the dual code
  • Partial codes
  • Properties of canword s
  • Various properties of the length
• Let's do some real combinatorics !!!
• Reduced words
  • canword s is reduced
• Braid monoid relations
  • reducing words for permutation
  • The cocode insertion algorithm
  • Straigthening a word
• The presentation of the symmetric groups

Library Combi.SymGroup.reprSn: Basic representations of the Symmetric Groups

• Basic representation of the Symmetric Groups
• Representation of dimension 1 and natural representation
• Representations of the symmetric Group for n = 0 and 1
• Representations of dimension 1 the symmetric Group for n > 1
• Representations of the symmetric Group for n=2

Library Combi.SymGroup.towerSn: The Tower of the Symmetric Groups

• The Tower of the Symmetric Groups
• External product of class functions
• Injection morphism of the tower of the symmetric groups
  • The tower is associative (upto isomorphism) with unit
• Restriction formula
• Induction formula

Library Combi.SymGroup.weak_order: The weak order on the Symmetric Group

• The weak order on the Symmetric Group

Library Combi.MPoly.antisym: Antisymmetric polynomials and Vandermonde product

• Antisymmetric polynomials
  • monomials and partitions
  • Change of scalar in multivariate polynomials
  • Characteristic of multivariate polynomials
• Symmetric and Antisymmetric multivariate polynomials
• Alternating polynomials
  • The leading monomial of an antisymmetric polynomial
  • Vandermonde product
  • Vandermonde matrix and determinant

Library Combi.MPoly.Cauchy: Cauchy formula for symmetric polynomials

• Cauchy formula for symmetric polynomials
  • Polynomials in two sets of variables
  • The Cauchy reproducing kernel
    • Cauchy formula for complete and monomial symmetric polynomials
    • Cauchy formula for Schur symmetric polynomials
    • Cauchy formula for power sum symmetric polynomials
• Cauchy kernel and scalar product of symmetric functions
  • Schur function are orthonormal

Library Combi.MPoly.homogsym: Homogenous Symmetric Polynomials

• The Space of Homogeneous Symmetric Polynomials
  • Homogeneous symmetric polynomials
  • Homogeneous symmetric polynomials as a vector space
  • Products of homogeneous symmetric polynomials
  • The omega involution
• The classical bases of homogeneous symmetric polynomials
  • Changing the base field
  • Extracting coords
  • Changing the number of variables
• The scalar product

Library Combi.MPoly.sympoly: Symmetric Polynomials

• The Ring of Symmetric Polynomials
  • Elementary symmetric polynomials
  • Complete homogeneous symmetric polynomials
  • Power sum symmetric polynomials
  • Monomial symmetric polynomials
    • Expansion of symmetric polynomials on monomials
  • Basis at degree 0
  • All basis agrees at degree 1
  • Schur symmetric polynomials
• Multiplicative bases.
• Littlewood-Richardson and Pieri rules
• Change of scalars
• Bases change formulas
  • Bases change between homogeneous and elementary
  • Newton formulas
  • Basis change from Schur to monomial
  • Basis change from complete and elementary to Schur
  • Basis change from complete to power sums
  • Symmetric polynomials expressed as polynomial in the elementary
  • Fundamental theorem of symmetric polynomials
• Change of the number of variables

Library Combi.MPoly.Schur_mpoly: Schur symmetric polynomials

• Combinatorial definition of Schur symmetric polynomials
  • Some particular Schur functions

Library Combi.MPoly.Schur_altdef: Alternants definition of Schur polynomials

• Definition of Schur polynomials as quotient of alternant and Kostka numbers
• Piery's rule for alternating polynomials
• Jacobi's definition of schur function
  • Schur polynomials are symmetric at last
• Kostka numbers
  • Converting between standard tableau and tableau over 'I_n.
• Restricting and extending tableaux
• Recursive computation of Kostka numbers
  • Inverse Kostka numbers
• Straightening of alternant polynomials

Library Combi.MPoly.MurnaghanNakayama: Murnaghan-Nakayama rule

• The Murnaghan-Nakayama rule
  • Product of an alternating polynomial and a power sum
  • Product of a Schur polynomial and a power sum
• Murnaghan-Nakayama coefficients
• Murnaghan-Nakayama rule

Library ALEA.Ccpo

• Ccpo.v: Specification and properties of a cpo
  • Ordered type
  • Definition and properties of x < y
    • Dual order
    • Order on functions
  • Monotonicity
    • Definition and properties
    • Type of monotonic functions
    • Monotonicity and dual order
    • Monotonicity and equality
    • Monotonic functions with 2 arguments
    • Strict monotonicity
  • Sequences
    • Usual order on natural numbers
    • Monotonicity and functions
  • Abstract relational notion of lubs
  • Basic operators of omega-cpos
    • Definition of cpos
    • Least upper bounds
    • Functional cpos
  • Cpo of monotonic functions
  • Continuity
    • Continuity
  • Cpo of continuous functions
  • Fixpoints
    • Iteration of functional
    • Induction principle
    • Function for conditionnal choice defined as a morphism

Library ALEA.Misc

• Misc.v: Preliminaries
  • Definition of iterator compn
  • Reducing if constructs
  • Classical reasoning
  • Extensional equality
• Preliminary lemmas relating the ordre on nat and N

Library ALEA.Qmeasure: Finite probabilities

• Definition of finite probabilities as measures with values in rational numbers
  • Properties of monadic operators
  • Properties of distributions
    • Expected properties of measures
    • Stability for substraction of unit and star
  • Definition of distribution
  • Properties of measures
  • Monadic operators for distributions
• Operations on distributions
  • Properties of monadic operators
• Examples of distributions
  • Flipping a coin:
  • Finite distributions given by points and rational coefficients
  • Uniform distribution on a non empty sequence of points
  • Uniform distribution between 0 and n included
• Distribution and big sums