Reconstructing partitions from pairwise products

DefinitionPairwise products of a multiset#✓fully proved

If a multiset \(s\) of natural numbers consists of \(x_1, \dots, x_k\), listed with multiplicity, then the pairwise products of \(s\) form the multiset of the products \(x_i x_j\) over all pairs of indices \(1 \le i < j \le k\); equal elements at different positions give separate products, and the result is empty when \(k < 2\).

Applied to the parts of a partition \(\lambda\), this gives the parts of the partition \(\mathrm{pre}_2(\lambda)\) of Li's note on multiset reconstruction.

def pairwiseProducts (s : Multiset ℕ) : Multiset ℕ :=
  (s.powersetCard 2).map Multiset.prod
Used by 2
Used byLi's lemma: reconstruction from the largest part and pairwise products · Li's theorem: partitions are determined by their pairwise products

TheoremLi's lemma: reconstruction from the largest part and pairwise products#●ready to prove

Let \(n\) be a positive integer and let \(\lambda\) and \(\mu\) be partitions of \(n\) with a common largest part, that is, some \(a\) is a part of both \(\lambda\) and \(\mu\) and no part of either exceeds \(a\). If the pairwise products of the parts of \(\lambda\) and the pairwise products of the parts of \(\mu\) form the same multiset, then \(\lambda = \mu\).

theorem_wanted partition_eq_of_pairwiseProducts_eq_of_max_eq
    {n : ℕ} (hn : 0 < n) (lam mu : Nat.Partition n)
    (hmax : ∃ a : ℕ, a ∈ lam.parts ∧ a ∈ mu.parts ∧
      (∀ x ∈ lam.parts, x ≤ a) ∧ (∀ x ∈ mu.parts, x ≤ a))
    (hpre : pairwiseProducts lam.parts = pairwiseProducts mu.parts) :
    lam = mu
Sources
  • Stella Jiahui Li, "A Note on Multiset Reconstruction from Pairwise Products and Total Sum", Lemma 1.
Uses 1
Statement usesPairwise products of a multiset

TheoremLi's theorem: partitions are determined by their pairwise products#●ready to prove

Let \(n\) be a positive integer and let \(\lambda\) and \(\mu\) be partitions of \(n\). The pairwise products of the parts of \(\lambda\) and the pairwise products of the parts of \(\mu\) form the same multiset if and only if \(\lambda = \mu\).

theorem_wanted partition_pairwiseProducts_eq_iff
    {n : ℕ} (hn : 0 < n) (lam mu : Nat.Partition n) :
    pairwiseProducts lam.parts = pairwiseProducts mu.parts ↔ lam = mu
Sources
  • Stella Jiahui Li, "A Note on Multiset Reconstruction from Pairwise Products and Total Sum", Theorem 1.
Uses 1
Statement usesPairwise products of a multiset
1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.