Overpartition congruences

TheoremOverpartitions of \(5n\) modulo \(5\), explicit form#✓fully proved

For every integer \(n \ge 1\), the number of pairs \((P, S)\), where \(P\) is a finite multiset of positive integers with sum \(5n\) and \(S\) is a finite set of natural numbers each belonging to \(P\), is congruent modulo \(5\) to \((-1)^n\) times the number of ordered triples \((x, y, z)\) of integers with \(x^2 + y^2 + z^2 = n\).

These pairs encode the overpartitions of \(5n\): \(P\) is the multiset of parts and \(S\) is the set of overlined part sizes.

public theorem overpartition_mul_five_mod_five
    (n : ℕ) (hn : 1 ≤ n) :
    Int.ModEq 5
      (Nat.card {
        p : Multiset ℕ × Finset ℕ //
          (∀ a ∈ p.1, 0 < a) ∧
          p.1.sum = 5 * n ∧
          ∀ a ∈ p.2, a ∈ p.1
      })
      (((-1 : ℤ) ^ n) * Nat.card {
        x : ℤ × ℤ × ℤ //
          x.1 ^ 2 + x.2.1 ^ 2 + x.2.2 ^ 2 = n
      })

Sources

• Liuquan Wang, "Another Proof of a Conjecture by Hirschhorn and Sellers on Overpartitions," Journal of Integer Sequences 17 (2014), Article 14.9.8, Theorem, lines 110–114. https://cs.uwaterloo.ca/journals/JIS/VOL17/Wang2/wang15.tex

Uses 1 · Used by 1

Proof usesJacobi triple product identity

Used byOverpartitions of \(5n\) modulo \(5\)

LemmaOverpartitions as pairs of a multiset and a set#✓fully proved

For every natural number \(m\), the number of overpartitions of \(m\) equals the number of pairs \((P, S)\) in which \(P\) is a finite multiset of positive integers with sum \(m\) and \(S\) is a finite set of natural numbers each belonging to \(P\).

public lemma natCard_eq_card_subtype (m : ℕ) :
    Nat.card (Nat.Overpartition m) =
      Nat.card { p : Multiset ℕ × Finset ℕ //
        (∀ a ∈ p.1, 0 < a) ∧ p.1.sum = m ∧ ∀ a ∈ p.2, a ∈ p.1 }

Uses 1 · Used by 1

Statement usesOverpartition

Used byOverpartitions of \(5n\) modulo \(5\)

LemmaThe three-square count counts all integer solutions#✓fully proved

For every natural number \(n\), the three-square representation count \(r_3(n)\) equals the number of ordered triples \((x, y, z)\) of integers with \(x^2 + y^2 + z^2 = n\).

public lemma threeSquareRepresentationCount_eq_natCard (n : ℕ) :
    threeSquareRepresentationCount n =
      Nat.card { x : ℤ × ℤ × ℤ //
        x.1 ^ 2 + x.2.1 ^ 2 + x.2.2 ^ 2 = (n : ℤ) }

Uses 1 · Used by 1

Statement usesNumber of representations as a sum of three squares

Used byOverpartitions of \(5n\) modulo \(5\)

TheoremOverpartitions of \(5n\) modulo \(5\)#✓fully proved

For every integer \(n \ge 1\), the number of overpartitions of \(5n\) is congruent modulo \(5\) to \((-1)^n r_3(n)\), where \(r_3(n)\) is the number of ordered triples \((x, y, z)\) of integers with \(x^2 + y^2 + z^2 = n\).

public theorem overpartition_card_mul_five_modEq (n : ℕ) (hn : 1 ≤ n) :
    Int.ModEq 5 (Nat.card (Nat.Overpartition (5 * n)))
      (((-1 : ℤ) ^ n) * Nat.threeSquareRepresentationCount n)

Uses 5

Statement usesOverpartition · Number of representations as a sum of three squares

Proof usesOverpartitions of \(5n\) modulo \(5\), explicit form · Overpartitions as pairs of a multiset and a set · The three-square count counts all integer solutions

TheoremLiang's congruences modulo 512 for overpartitions#●ready to prove

For all natural numbers \(\alpha\) and \(n\), the number \(\overline{p}(m)\) of overpartitions of \(m\) satisfies \(\overline{p}(3^{8\alpha+7}(24n+5)) \equiv 0 \pmod{512}\) and \(\overline{p}(3^{8\alpha+7}(24n+13)) \equiv 0 \pmod{512}\).

public theorem_wanted overpartition_three_pow_congr_zero_mod_512 (α n : ℕ) :
    512 ∣ Nat.card (Nat.Overpartition (3 ^ (8 * α + 7) * (24 * n + 5))) ∧
      512 ∣ Nat.card (Nat.Overpartition (3 ^ (8 * α + 7) * (24 * n + 13)))

Sources

• Xue Liang, Congruences Modulo 512 for the Overpartition Function, INTEGERS 25 (2025), Article A76, Theorem 1.

Uses 1

Statement usesOverpartition

TheoremEta-quotient identity in the powers \(q^3\), \(q^6\), \(q^9\) and \(q^{18}\)#●ready to prove

Let \(q\) be a complex number with \(|q| < 1\), and for each integer \(k \ge 1\) write \(E_k = (q^k; q^k)_\infty\), the infinite q-Pochhammer symbol \(\prod_{n=0}^{\infty} (1 - q^{k(n+1)})\). Then

\[ \frac{E_6^3 E_9^6}{E_3^3 E_{18}^3} = \frac{E_6^8 E_9}{E_3^4 E_{18}^2} - q^3 \, \frac{E_{18}^6}{E_9^3}. \]

public theorem_wanted eulerFunction_six_cube_nine_six_div_eq (q : ℂ) (hq : ‖q‖ < 1) :
    let E : ℕ → ℂ := fun k => if hk : k = 0 then 1 else
      QPochhammer.qPochhammerInf (q ^ k) (q ^ k)
        (by rw [norm_pow]; exact pow_lt_one₀ (norm_nonneg q) hq hk)
    E 6 ^ 3 * E 9 ^ 6 / (E 3 ^ 3 * E 18 ^ 3) =
      E 6 ^ 8 * E 9 / (E 3 ^ 4 * E 18 ^ 2) - q ^ 3 * (E 18 ^ 6 / E 9 ^ 3)

Sources

• Xue Liang, Congruences Modulo 512 for the Overpartition Function, INTEGERS 25 (2025), Article A76, Lemma 1, identity (10). Identity (9) of the same lemma is ramanujanPsi_three_dissection (OverpartitionSpt2CongruencesWanted).

Uses 1

Statement usesInfinite q-Pochhammer symbol

TheoremThree-dissection of \((q;q)_\infty / (q^2;q^2)_\infty^2\)#●ready to prove

Let \(q\) be a complex number with \(|q| < 1\), and for each integer \(k \ge 1\) write \(E_k = (q^k; q^k)_\infty\), the infinite q-Pochhammer symbol \(\prod_{n=0}^{\infty} (1 - q^{k(n+1)})\). Then

\[ \frac{E_1}{E_2^2} = \frac{E_3^2 E_9^3}{E_6^6} - q \, \frac{E_3^3 E_{18}^3}{E_6^7} + q^2 \, \frac{E_3^4 E_{18}^6}{E_6^8 E_9^3}. \]

public theorem_wanted eulerFunction_one_div_two_sq_eq (q : ℂ) (hq : ‖q‖ < 1) :
    let E : ℕ → ℂ := fun k => if hk : k = 0 then 1 else
      QPochhammer.qPochhammerInf (q ^ k) (q ^ k)
        (by rw [norm_pow]; exact pow_lt_one₀ (norm_nonneg q) hq hk)
    E 1 / E 2 ^ 2 =
      E 3 ^ 2 * E 9 ^ 3 / E 6 ^ 6 - q * (E 3 ^ 3 * E 18 ^ 3 / E 6 ^ 7) +
        q ^ 2 * (E 3 ^ 4 * E 18 ^ 6 / (E 6 ^ 8 * E 9 ^ 3))

Sources

• Xue Liang, Congruences Modulo 512 for the Overpartition Function, INTEGERS 25 (2025), Article A76, Lemma 1, identity (11).

Uses 1

Statement usesInfinite q-Pochhammer symbol

4 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.