Ramanujan's partition congruences

TheoremTwice a triangular number#✓fully proved

For every natural number \(a\), \(2\binom{a+1}{2} = a(a+1)\).

theorem two_mul_choose_two_succ (a : ℕ) : 2 * (a + 1).choose 2 = a * (a + 1)
Used by 5
Used byCoefficients of Jacobi's cube series at triangular numbers · Jacobi's cube identity · Ramanujan's congruence modulo 11 · Ramanujan's congruence modulo 5 · Ramanujan's congruence modulo 7

DefinitionJacobi's cube series#✓fully proved

Jacobi's cube series is the formal power series \(J(X) = \sum_{t \ge 0} (-1)^t (2t+1) X^{t(t+1)/2}\) in \(\mathbb{Z}[[X]]\): for each natural number \(t\) its coefficient at the triangular number \(t(t+1)/2\) is \((-1)^t (2t+1)\), and all its other coefficients are \(0\).

noncomputable def jacobiCubeSeries : PowerSeries ℤ :=
  PowerSeries.mk fun b =>
    ∑ t ∈ Finset.range (b + 1),
      (if (t + 1).choose 2 = b then (-1 : ℤ) ^ t * (2 * t + 1) else 0)
Used by 7
Used byVanishing coefficients of Jacobi's cube series · Coefficients of Jacobi's cube series at triangular numbers · Jacobi's cube identity · Ramanujan's congruence modulo 11 · Ramanujan's congruence modulo 5 · Ramanujan's congruence modulo 7 · Jacobi's identity for the cube of Euler's product

TheoremCoefficients of Jacobi's cube series at triangular numbers#✓fully proved

Let \(J(X)\) be Jacobi's cube series. For every natural number \(t\), the coefficient of \(X^{t(t+1)/2}\) in \(J(X)\) is \((-1)^t (2t+1)\).

theorem coeff_jacobiCubeSeries_triangle (t : ℕ) :
    PowerSeries.coeff ((t + 1).choose 2) jacobiCubeSeries = (-1 : ℤ) ^ t * (2 * t + 1)
Uses 2 · Used by 4
Statement usesJacobi's cube series
Proof usesTwice a triangular number
Used byRamanujan's congruence modulo 11 · Ramanujan's congruence modulo 5 · Ramanujan's congruence modulo 7 · Jacobi's identity for the cube of Euler's product

TheoremVanishing coefficients of Jacobi's cube series#✓fully proved

Let \(J(X)\) be Jacobi's cube series. If a natural number \(b\) is not of the form \(t(t+1)/2\) for any natural number \(t\), then the coefficient of \(X^b\) in \(J(X)\) is \(0\).

theorem coeff_jacobiCubeSeries_eq_zero {b : ℕ} (hb : ∀ t : ℕ, (t + 1).choose 2 ≠ b) :
    PowerSeries.coeff b jacobiCubeSeries = 0
Uses 1 · Used by 4
Statement usesJacobi's cube series
Used byRamanujan's congruence modulo 11 · Ramanujan's congruence modulo 5 · Ramanujan's congruence modulo 7 · Jacobi's identity for the cube of Euler's product

TheoremJacobi's cube identity#✓fully proved

Let \(E(X) = \sum_{k \in \mathbb{Z}} (-1)^k X^{k(3k-1)/2}\) be Euler's pentagonal series and \(J(X) = \sum_{t \ge 0} (-1)^t (2t+1) X^{t(t+1)/2}\) Jacobi's cube series, both in \(\mathbb{Z}[[X]]\). Then \(E(X)^3 = J(X)\).

theorem pentagonalSeries_pow_three :
    PowerSeries.pentagonalSeries ℤ ^ 3 = jacobiCubeSeries
Uses 11 · Used by 4
Statement usesJacobi's cube series
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\) · Gaussian binomial coefficients with \(M = 0\) · Finite \(Q\)-Pochhammer symbol · Recursion for the finite \(Q\)-Pochhammer symbol · Twice a triangular number
Used byRamanujan's congruence modulo 11 · Ramanujan's congruence modulo 5 · Ramanujan's congruence modulo 7 · Jacobi's identity for the cube of Euler's product

TheoremPartition congruences from a power of Euler's series#✓fully proved

Let \(p\) be a prime, let \(r < p\) be a natural number, and let \(E(X) = \sum_{k \in \mathbb{Z}} (-1)^k X^{k(3k-1)/2}\) be Euler's pentagonal series in \(\mathbb{Z}[[X]]\). If \(p\) divides the coefficient of \(X^{pm+r}\) in \(E(X)^{p-1}\) for every natural number \(m\), then \(p\) divides the number of partitions of \(pm + r\) for every natural number \(m\).

theorem dvd_partitionFunction_of_dvd_coeff_pentagonalSeries_pow
    (p r : ℕ) [Fact (Nat.Prime p)] (hr : r < p)
    (hvan : ∀ m : ℕ, (p : ℤ)
      ∣ PowerSeries.coeff (p * m + r)
        (PowerSeries.pentagonalSeries ℤ ^ (p - 1))) (m : ℕ) :
    p ∣ Fintype.card (Nat.Partition (p * m + r))
Uses 2 · Used by 3
Proof usesEuler's identity for the partition generating function · The partition function
Used byRamanujan's congruence modulo 11 · Ramanujan's congruence modulo 5 · Ramanujan's congruence modulo 7

TheoremRamanujan's congruence modulo 5#✓fully proved

For every natural number \(m\), the number of partitions of \(5m + 4\) is divisible by \(5\).

theorem ramanujan_partition_congruence_mod_five (m : ℕ) :
    Fintype.card (Nat.Partition (5 * m + 4)) ≡ 0 [MOD 5]
Sources
  • Hartosh Singh Bal and Gaurav Bhatnagar, JIS 27 (2024), Art. 24.1.6, lines 801–804. Live source: https://cs.uwaterloo.ca/journals/JIS/VOL27/Bhatnagar/bhat4.tex
Uses 6
Proof usesVanishing coefficients of Jacobi's cube series · Coefficients of Jacobi's cube series at triangular numbers · Partition congruences from a power of Euler's series · Jacobi's cube series · Jacobi's cube identity · Twice a triangular number

TheoremRamanujan's congruence modulo 7#✓fully proved

For every natural number \(m\), the number of partitions of \(7m + 5\) is divisible by \(7\).

theorem ramanujan_partition_congruence_mod_seven (m : ℕ) :
    Fintype.card (Nat.Partition (7 * m + 5)) ≡ 0 [MOD 7]
Sources
  • S. Ramanujan, "Some properties of p(n), the number of partitions of n", Proceedings of the Cambridge Philosophical Society 19 (1919), 207–210, where the congruence is stated and proved. The proof follows Ramanujan's argument there: the sixth power of Euler's product is the square of Jacobi's cube series, and a sum of two squares divisible by 7 has both terms divisible by 7.
Uses 6
Proof usesVanishing coefficients of Jacobi's cube series · Coefficients of Jacobi's cube series at triangular numbers · Partition congruences from a power of Euler's series · Jacobi's cube series · Jacobi's cube identity · Twice a triangular number

TheoremRamanujan's congruence modulo 11#✓fully proved

For every natural number \(m\), the number of partitions of \(11m + 6\) is divisible by \(11\).

Proof: We follow Hirschhorn's Section 2 residue-section argument, using Euler's pentagonal number theorem and Jacobi's cube identity.

public theorem ramanujan_partition_congruence_mod_eleven (m : ℕ) :
    Fintype.card (Nat.Partition (11 * m + 6)) ≡ 0 [MOD 11]
Sources
  • https://en.wikipedia.org/wiki/Ramanujan%27s_congruences
Uses 6
Proof usesVanishing coefficients of Jacobi's cube series · Coefficients of Jacobi's cube series at triangular numbers · Partition congruences from a power of Euler's series · Jacobi's cube series · Jacobi's cube identity · Twice a triangular number
9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.