Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

First letters at a fixed inversion number

Abstract

For k<n, the mean first letter at inversion number k is M(n+1,k)/M(n,k).

Permutations are Equiv.Perm (Fin n), with positions numbered from zero. The existing PSW.word sends a permutation pi to List.ofFn (fun i => (pi i).val + 1), so its entries are the source’s one-based letters. D5.S1.Digit.Carry.ListInversions.inv counts strictly inverted pairs of positions. Nat.cast in the formulas below has codomain Q, the rational field. The function List.headD returns its default zero on an empty word; k0.

Definition 1.1 (Mahonian cardinalities).

Formalization. D5/S3/Combinatorics/Permutation/KageyInversionFirstLetter.M (✓ std3).

Citation. Peter Kagey (2021). Expected value of letters of permutations with a given number of k-cycles. DOI: 10.48550/arXiv.2112.05281. URL: https://arxiv.org/abs/2112.05281v1.

Commentary.

Section 5.2, page 20: “where M(n, k), as above, is the number of permutations w ∈ S_n such that inv(w) = k.” The finite set contains each permutation once and retains exactly inversion number k.

Definition 1.2 (The conditional mean).

Formalization. D5/S3/Combinatorics/Permutation/KageyInversionFirstLetter.E (✓ std3).

Citation. Peter Kagey (2021). Expected value of letters of permutations with a given number of k-cycles. DOI: 10.48550/arXiv.2112.05281. URL: https://arxiv.org/abs/2112.05281v1.

Commentary.

Section 5.2, page 20: “Because the expected value of the first letter is given by the weighted sum of the permutations with mah(w) = k divided by the number of such permutations, E[π(1) | π ∈ S_n, mah(π) = k] has a denominator that is (a factor of) M(n, k), the number of permutations of w ∈ S_n such that inv(w) = k.” Here mah is inv. Each first letter is cast to Q before summation, and M(n,k) is cast to Q before division. Rational division is total, including when the finite set is empty.

Definition 1.3 (Kagey’s Conjecture 5.1).

Formalization. D5/S3/Combinatorics/Permutation/KageyInversionFirstLetter.claim (✓ std3).

Citation. Peter Kagey (2021). Expected value of letters of permutations with a given number of k-cycles. DOI: 10.48550/arXiv.2112.05281. URL: https://arxiv.org/abs/2112.05281v1.

Commentary.

Conjecture 5.1, page 20: “For fixed k and n > k, the expected value of the first letter of a permutation with a given number of inversions satisfies a rational function in n given by E[π(1) | π ∈ S_n, inv(π) = k] = M(n + 1, k)/M(n, k), where M(n, k), as above, is the number of permutations w ∈ S_n such that inv(w) = k.” Both k and n range over natural numbers; k<n is the complete hypothesis.

Theorem 1.4 (The first-letter expectation identity).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Permutation/KageyInversionFirstLetter.result (✓ std3). ∎

Resolves. Problems/kagey-2021-inversion-first-letter-conjecture-5-1 (proved) by D5/S3/Combinatorics/Permutation/KageyInversionFirstLetter.result.

Source. Repository-derived.

Acknowledgement. Peter Kagey (2021). Expected value of letters of permutations with a given number of k-cycles. DOI: 10.48550/arXiv.2112.05281. URL: https://arxiv.org/abs/2112.05281v1.

Commentary.

Deleting first letter j removes j−1 inversions. Two successive insertions with total inversion contribution t have t+1 choices when t≤k<n. Their count equals the first-letter weight. Thus the natural weighted numerator is M(n+1,k); casting that identity to Q proves the displayed equality.

References