Partition identities

Theorems equating counts of two classes of partitions: Euler, MacMahon, Andrews, Andrews–Lewis, Rogers–Ramanujan, Stanley and Elder theorems, polarized and 2-distant partitions, colored Euler-type identities and Merca's sums of different parts.

TheoremAndrews–Lewis identity#✓fully proved

For every natural number \(n\), the number of partitions of \(n\) into odd parts in which each part occurs at most three times equals the number of partitions of \(n\) into parts congruent to \(1\) or \(3\) modulo \(4\) such that for no natural number \(j \le n\) are both \(4j + 1\) and \(4j + 3\) parts.

theorem card_odd_countRestricted_four_eq_card_mod_four_pair_excluding
    (n : ℕ) :
    (Nat.Partition.odds n ∩ Nat.Partition.countRestricted n 4).card =
      (Finset.univ.filter fun p : Nat.Partition n ↦
        (∀ i ∈ p.parts, i % 4 = 1 ∨ i % 4 = 3) ∧
          ∀ j ∈ Finset.range (n + 1),
            ¬ (4 * j + 1 ∈ p.parts ∧ 4 * j + 3 ∈ p.parts)).card

Sources

the Andrews–Lewis identity (G. E. Andrews and R. P. Lewis, "An algebraic identity of F. H. Jackson and its implications for partitions," Discrete Math. 232 (2001), 77–83) as quoted in Michael D. Hirschhorn and James A. Sellers, "A Congruence Modulo 3 for Partitions into Distinct Non-Multiples of Four," Journal of Integer Sequences 17 (2014), Article 14.9.6, Theorem, lines 99–102. https://cs.uwaterloo.ca/journals/JIS/VOL17/Sellers/sellers32.tex

TheoremPartitions with 2-distant parts and polarized partitions#✓fully proved

For every natural number \(n\), the number of partitions of \(n\) into distinct parts any two of which differ by at least \(2\) equals the number of polarized partitions of \(n\), that is, partitions of \(n\) into distinct parts in which every even part is greater than twice the number of odd parts.

theorem partitions_two_distant_eq_polarized (n : ℕ) :
    Fintype.card {p : Nat.Partition n //
      p.parts.Nodup ∧ ∀ a ∈ p.parts, ∀ b ∈ p.parts, a < b → a + 2 ≤ b} =
      Fintype.card {p : Nat.Partition n //
        p.parts.Nodup ∧ ∀ e ∈ p.parts, e % 2 = 0 →
          2 * (p.parts.filter (fun i => i % 2 = 1)).card < e}

Sources

Ivica Martinjak and Dragutin Svrtan, "New Identities for the Polarized Partitions and Partitions with d-Distant Parts," Journal of Integer Sequences 17 (2014), Article 14.11.4, Theorem 1, lines 150–155, https://cs.uwaterloo.ca/journals/JIS/VOL17/Martinjak/mart3.tex.

TheoremRogers–Ramanujan identity (first form)#✓fully proved

For every natural number \(n\), the number of partitions of \(n\) into distinct parts, any two of which differ by at least \(2\), equals the number of partitions of \(n\) all of whose parts are congruent to \(1\) or \(4\) modulo \(5\).

public theorem rogers_ramanujan_difference_two_vs_one_four (n : ℕ) :
    (Finset.univ.filter (fun p : Nat.Partition n =>
      p.parts.Nodup ∧ ∀ a ∈ p.parts, ∀ b ∈ p.parts, a < b → a + 2 ≤ b)).card =
    (Finset.univ.filter (fun p : Nat.Partition n =>
      ∀ m ∈ p.parts, m % 5 = 1 ∨ m % 5 = 4)).card

Sources

George E. Andrews and David Newman, "The Minimal Excludant in Integer Partitions," Journal of Integer Sequences 23 (2020), Article 20.2.3, quoted Rogers–Ramanujan theorem at lines 173–178. Public TeX URL: https://cs.uwaterloo.ca/journals/JIS/VOL23/Andrews/andrews5.tex

Uses 7

Proof usesGaussian binomial coefficient · Gaussian binomial coefficients vanish when \(k > M\) · Product formula for Gaussian binomial coefficients · Diagonal Gaussian binomial coefficients · \(Q\)-Pascal recursion for Gaussian binomial coefficients · Gaussian binomial coefficients with \(k = 0\) · Finite \(Q\)-Pochhammer symbol

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.