Analogs of the 5-core partition function

DefinitionRamanujan's general theta function at powers of q#✓fully proved

For positive integers \(i\) and \(j\), \(f(q^i, q^j)\) is the integer power series \(\sum_{n \in \mathbb{Z}} q^{i n(n+1)/2 + j n(n-1)/2}\), that is, Ramanujan's \(f(a, b) = \sum_{n \in \mathbb{Z}} a^{n(n+1)/2} b^{n(n-1)/2}\) at \(a = q^i\) and \(b = q^j\).

Since \(i, j \ge 1\), only integers \(n\) with \(|n| \le m\) contribute to the coefficient of \(q^m\), so each coefficient is a finite count.

def ramanujanThetaPow (i j : ℕ+) : ℤ⟦X⟧ :=
  mk fun m => (((Finset.Icc (-(m : ℤ)) m).filter fun n =>
    ((i : ℕ) : ℤ) * (n * (n + 1) / 2) + ((j : ℕ) : ℤ) * (n * (n - 1) / 2) = m).card : ℤ)
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Section 1 (definition of f(a, b)).
Used by 7
Used byConstant term of Ramanujan's theta function · Generating function of the \(\varphi\)-analog of the 5-core counts · Generating function of the \(\psi\)-analog of the 5-core counts · The φ-analog of the 5-core partition function · The ψ-analog of the 5-core partition function · 5-dissections of Ramanujan's theta functions φ and ψ · Theta-function identities of level 5

DefinitionThe 5-core counts#✓fully proved

For a natural number \(n\), \(c_5(n)\) is the coefficient of \(q^n\) in the integer power series \(f_5^5 / f_1\), where \(f_k = \prod_{m \ge 1} (1 - q^{km})\) is the Euler product. The series \(f_5^5 / f_1\) is the generating function of 5-core partitions.

noncomputable def fiveCoreCount (n : ℕ) : ℤ :=
  coeff n (qEulerProduct 5 ^ 5 * invOfUnit (pentagonalSeries ℤ) 1)
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Section 1, equation for ∑ c_t(n) q^n with t = 5 (OEIS A053723).
Uses 1 · Used by 4
Statement usesThe Euler products of partition theory
Used byTwo identities for the 5-core counts · Generating function of the 5-core counts · The \(\varphi\)-analog of the 5-core counts in terms of the 5-core counts · Identities relating the ψ-analog to the 5-core counts and the φ-analog

DefinitionThe φ-analog of the 5-core partition function#✓fully proved

Let \(\varphi(q) = \sum_{n \in \mathbb{Z}} q^{n^2}\) be Ramanujan's theta function. For a natural number \(n\), \(\bar a_5(n)\) is the coefficient of \(q^n\) in the integer power series \(\varphi^5(-q^5)/\varphi(-q)\) (the denominator has constant term \(1\), so the quotient is a power series).

noncomputable def phiFiveCoreAnalog (n : ℕ) : ℤ :=
  coeff n (expand 5 (by norm_num) (rescale (-1) (ramanujanThetaPow 1 1)) ^ 5 *
    invOfUnit (rescale (-1) (ramanujanThetaPow 1 1)) 1)
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Section 1, equation (at) (OEIS A368490).
Uses 1 · Used by 6
Statement usesRamanujan's general theta function at powers of q
Used byGenerating function of the \(\varphi\)-analog of the 5-core counts · Congruences for the \(\varphi\)-analog of the 5-core counts · The \(\varphi\)-analog of the 5-core counts in terms of the 5-core counts · The \(\varphi\)-analog in terms of the \(\psi\)-analog of the 5-core counts · Recurrence for the \(\varphi\)-analog of the 5-core counts along powers of 5 · Identities relating the ψ-analog to the 5-core counts and the φ-analog

DefinitionThe ψ-analog of the 5-core partition function#✓fully proved

Let \(\psi(q) = \sum_{n \in \mathbb{Z}} q^{2n^2 - n} = \sum_{n \ge 0} q^{n(n+1)/2}\) be Ramanujan's theta function. For a natural number \(n\), \(\bar b_5(n)\) is the coefficient of \(q^n\) in the integer power series \(\psi^5(-q^5)/\psi(-q)\) (the denominator has constant term \(1\), so the quotient is a power series).

noncomputable def psiFiveCoreAnalog (n : ℕ) : ℤ :=
  coeff n (expand 5 (by norm_num) (rescale (-1) (ramanujanThetaPow 1 3)) ^ 5 *
    invOfUnit (rescale (-1) (ramanujanThetaPow 1 3)) 1)
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Section 1, equation (bt) (OEIS A368495).
Uses 1 · Used by 7
Statement usesRamanujan's general theta function at powers of q
Used byGenerating function of the \(\psi\)-analog of the 5-core counts · The \(\varphi\)-analog in terms of the \(\psi\)-analog of the 5-core counts · Congruences for the ψ-analog of the 5-core partition function · A recurrence for the ψ-analog of the 5-core partition function along powers of 5 · A doubling identity for the ψ-analog of the 5-core partition function · Identities relating the ψ-analog to the 5-core counts and the φ-analog · Sign densities of the ψ-analog of the 5-core partition function

TheoremConstant term of Ramanujan's theta function#✓fully proved

For all positive integers \(i\) and \(j\), the integer power series \(f(q^i, q^j) = \sum_{n \in \mathbb{Z}} q^{i n(n+1)/2 + j n(n-1)/2}\) has constant term \(1\): only \(n = 0\) contributes to \(q^0\).

theorem constantCoeff_ramanujanThetaPow (i j : ℕ+) : constantCoeff (ramanujanThetaPow i j) = 1
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Section 1.
Uses 1 · Used by 2
Statement usesRamanujan's general theta function at powers of q
Used byGenerating function of the \(\varphi\)-analog of the 5-core counts · Generating function of the \(\psi\)-analog of the 5-core counts

TheoremGenerating function of the 5-core counts#✓fully proved

Let \(f_k = \prod_{m \ge 1} (1 - q^{km})\) and let \(c_5(n)\) be the coefficient of \(q^n\) in \(f_5^5 / f_1\). Then, as integer power series, \(\left(\sum_{n \ge 0} c_5(n) q^n\right) f_1 = f_5^5\), where \(f_1\) is written as the pentagonal series \(\sum_{j \in \mathbb{Z}} (-1)^j q^{j(3j-1)/2}\).

theorem mk_fiveCoreCount_mul : mk fiveCoreCount * pentagonalSeries ℤ = qEulerProduct 5 ^ 5
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Section 1.
Uses 2
Statement usesThe 5-core counts · The Euler products of partition theory

TheoremGenerating function of the \(\varphi\)-analog of the 5-core counts#✓fully proved

Let \(\varphi(q) = \sum_{n \in \mathbb{Z}} q^{n^2}\) and let \(\bar a_5(n)\) be the coefficient of \(q^n\) in \(\varphi(-q^5)^5 / \varphi(-q)\). Then, as integer power series, \(\left(\sum_{n \ge 0} \bar a_5(n) q^n\right) \varphi(-q) = \varphi(-q^5)^5\).

theorem mk_phiFiveCoreAnalog_mul :
    mk phiFiveCoreAnalog * rescale (-1) (ramanujanThetaPow 1 1) =
      expand 5 (by norm_num) (rescale (-1) (ramanujanThetaPow 1 1)) ^ 5
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Section 1, equation (at).
Uses 3
Statement usesThe φ-analog of the 5-core partition function · Ramanujan's general theta function at powers of q
Proof usesConstant term of Ramanujan's theta function

TheoremGenerating function of the \(\psi\)-analog of the 5-core counts#✓fully proved

Let \(\psi(q) = \sum_{n \in \mathbb{Z}} q^{n(2n-1)}\) and let \(\bar b_5(n)\) be the coefficient of \(q^n\) in \(\psi(-q^5)^5 / \psi(-q)\). Then, as integer power series, \(\left(\sum_{n \ge 0} \bar b_5(n) q^n\right) \psi(-q) = \psi(-q^5)^5\).

theorem mk_psiFiveCoreAnalog_mul :
    mk psiFiveCoreAnalog * rescale (-1) (ramanujanThetaPow 1 3) =
      expand 5 (by norm_num) (rescale (-1) (ramanujanThetaPow 1 3)) ^ 5
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Section 1, equation (bt).
Uses 3
Statement usesThe ψ-analog of the 5-core partition function · Ramanujan's general theta function at powers of q
Proof usesConstant term of Ramanujan's theta function

TheoremThe \(\varphi\)-analog of the 5-core counts in terms of the 5-core counts#●ready to prove

Let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), let \(c_5(n)\) be the coefficient of \(q^n\) in \(f_5^5 / f_1\), let \(\varphi(q) = \sum_{n \in \mathbb{Z}} q^{n^2}\) and let \(\bar a_5(n)\) be the coefficient of \(q^n\) in \(\varphi(-q^5)^5 / \varphi(-q)\). For every natural number \(n\), \(\bar a_5(5n+2) = 4\, c_5(5n+1)\), \(\bar a_5(5n+3) = 4\, c_5(5n+2)\), \(\bar a_5(10n+1) = 2\, c_5(10n)\), \(\bar a_5(10n+9) = 2\, c_5(10n+8)\), \(\bar a_5(20n+6) = 10\, c_5(10n+2)\) and \(\bar a_5(20n+14) = 10\, c_5(10n+6)\).

public theorem_wanted phiFiveCoreAnalog_eq_fiveCoreCount (n : ℕ) :
    phiFiveCoreAnalog (5 * n + 2) = 4 * fiveCoreCount (5 * n + 1) ∧
      phiFiveCoreAnalog (5 * n + 3) = 4 * fiveCoreCount (5 * n + 2) ∧
      phiFiveCoreAnalog (10 * n + 1) = 2 * fiveCoreCount (10 * n) ∧
      phiFiveCoreAnalog (10 * n + 9) = 2 * fiveCoreCount (10 * n + 8) ∧
      phiFiveCoreAnalog (20 * n + 6) = 10 * fiveCoreCount (10 * n + 2) ∧
      phiFiveCoreAnalog (20 * n + 14) = 10 * fiveCoreCount (10 * n + 6)
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Theorem 2 (jis-2024-24.4.5-thm-2).
Uses 2
Statement usesThe 5-core counts · The φ-analog of the 5-core partition function

TheoremRecurrence for the \(\varphi\)-analog of the 5-core counts along powers of 5#●ready to prove

Let \(\varphi(q) = \sum_{n \in \mathbb{Z}} q^{n^2}\) and let \(\bar a_5(n)\) be the coefficient of \(q^n\) in \(\varphi(-q^5)^5 / \varphi(-q)\). For every natural number \(k \ge 2\) and every natural number \(n\), \(\bar a_5(5^k n) = \frac{5^k - 1}{4}\, \bar a_5(5n) - \frac{5^k - 5}{4}\, \bar a_5(n)\). Both quotients are integers.

public theorem_wanted phiFiveCoreAnalog_five_pow_mul {k : ℕ} (hk : 2 ≤ k) (n : ℕ) :
    phiFiveCoreAnalog (5 ^ k * n) =
      ((5 ^ k - 1) / 4 : ℤ) * phiFiveCoreAnalog (5 * n) -
        ((5 ^ k - 5) / 4 : ℤ) * phiFiveCoreAnalog n
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Theorem 2 (jis-2024-24.4.5-thm-2).
Uses 1
Statement usesThe φ-analog of the 5-core partition function

TheoremCongruences for the \(\varphi\)-analog of the 5-core counts#●ready to prove

Let \(\varphi(q) = \sum_{n \in \mathbb{Z}} q^{n^2}\) and let \(\bar a_5(n)\) be the coefficient of \(q^n\) in \(\varphi(-q^5)^5 / \varphi(-q)\). For every natural number \(k \ge 2\) and every natural number \(n\), \(\bar a_5(20n+6) \equiv 0 \pmod{10}\), \(\bar a_5(20n+14) \equiv 0 \pmod{10}\) and \(4\, \bar a_5(5^k n) \equiv 5\, \bar a_5(n) - \bar a_5(5n) \pmod{5^k}\).

public theorem_wanted phiFiveCoreAnalog_congruences {k : ℕ} (hk : 2 ≤ k) (n : ℕ) :
    phiFiveCoreAnalog (20 * n + 6) ≡ 0 [ZMOD 10] ∧
      phiFiveCoreAnalog (20 * n + 14) ≡ 0 [ZMOD 10] ∧
      4 * phiFiveCoreAnalog (5 ^ k * n) ≡ 5 * phiFiveCoreAnalog n - phiFiveCoreAnalog (5 * n)
        [ZMOD 5 ^ k]
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Corollary 3 (jis-2024-24.4.5-cor-3).
Uses 1
Statement usesThe φ-analog of the 5-core partition function

TheoremA doubling identity for the ψ-analog of the 5-core partition function#●ready to prove

Let \(\bar b_5(n)\) be the coefficient of \(q^n\) in \(\psi^5(-q^5)/\psi(-q)\), where \(\psi(q) = \sum_{n \ge 0} q^{n(n+1)/2}\). For every natural number \(n\), \(\bar b_5(4n+3) = 2 \bar b_5(2n)\).

public theorem_wanted psiFiveCoreAnalog_four_mul_add_three (n : ℕ) :
    psiFiveCoreAnalog (4 * n + 3) = 2 * psiFiveCoreAnalog (2 * n)
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Theorem 4 (jis-2024-24.4.5-thm-4).
Uses 1
Statement usesThe ψ-analog of the 5-core partition function

TheoremA recurrence for the ψ-analog of the 5-core partition function along powers of 5#●ready to prove

Let \(\bar b_5(n)\) be the coefficient of \(q^n\) in \(\psi^5(-q^5)/\psi(-q)\), where \(\psi(q) = \sum_{n \ge 0} q^{n(n+1)/2}\). For every integer \(k \ge 2\) and every natural number \(n\), \(\bar b_5(5^k(n+3) - 3) = \frac{5^k - 1}{4} \bar b_5(5n+12) - \frac{5^k - 5}{4} \bar b_5(n)\); both quotients are integers.

public theorem_wanted psiFiveCoreAnalog_five_pow_mul {k : ℕ} (hk : 2 ≤ k) (n : ℕ) :
    psiFiveCoreAnalog (5 ^ k * (n + 3) - 3) =
      ((5 ^ k - 1) / 4 : ℤ) * psiFiveCoreAnalog (5 * n + 12) -
        ((5 ^ k - 5) / 4 : ℤ) * psiFiveCoreAnalog n
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Theorem 4 (jis-2024-24.4.5-thm-4).
Uses 1
Statement usesThe ψ-analog of the 5-core partition function

TheoremIdentities relating the ψ-analog to the 5-core counts and the φ-analog#●ready to prove

Let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), \(\varphi(q) = \sum_{n \in \mathbb{Z}} q^{n^2}\) and \(\psi(q) = \sum_{n \ge 0} q^{n(n+1)/2}\), and let \(c_5(n)\), \(\bar a_5(n)\) and \(\bar b_5(n)\) be the coefficients of \(q^n\) in \(f_5^5/f_1\), \(\varphi^5(-q^5)/\varphi(-q)\) and \(\psi^5(-q^5)/\psi(-q)\). Then for every natural number \(n\): \(\bar b_5(4n+1) = c_5(n) - 2 \bar b_5(2n-1)\), where the last term is read as \(0\) for \(n = 0\); \(2 \bar b_5(10n) = c_5(10n+2)\); \(\bar b_5(10n+1) = c_5(5n+1)\); \(4 \bar b_5(10n+2) = \bar a_5(2n+1) + 2 c_5(2n)\); \(\bar b_5(10n+3) = c_5(5n+2)\); \(2 \bar b_5(10n+4) = c_5(10n+6)\); \(\bar b_5(10n+6) = \bar b_5(10n+8) = 0\); \(\bar b_5(20n+5) = -c_5(5n+1)\); \(2 \bar b_5(20n+7) = \bar a_5(2n+1) + 2 c_5(2n)\); \(\bar b_5(20n+9) = -c_5(5n+2)\); and \(\bar b_5(20n+15) = \bar b_5(20n+19) = 0\).

MetaMathlibExt.psiFiveCoreAnalog_identities · 17 lines 
public theorem_wanted psiFiveCoreAnalog_identities (n : ℕ) :
    psiFiveCoreAnalog (4 * n + 1) =
        fiveCoreCount n - 2 * (if n = 0 then 0 else psiFiveCoreAnalog (2 * n - 1)) ∧
      2 * psiFiveCoreAnalog (10 * n) = fiveCoreCount (10 * n + 2) ∧
      psiFiveCoreAnalog (10 * n + 1) = fiveCoreCount (5 * n + 1) ∧
      4 * psiFiveCoreAnalog (10 * n + 2) =
        phiFiveCoreAnalog (2 * n + 1) + 2 * fiveCoreCount (2 * n) ∧
      psiFiveCoreAnalog (10 * n + 3) = fiveCoreCount (5 * n + 2) ∧
      2 * psiFiveCoreAnalog (10 * n + 4) = fiveCoreCount (10 * n + 6) ∧
      psiFiveCoreAnalog (10 * n + 6) = 0 ∧
      psiFiveCoreAnalog (10 * n + 8) = 0 ∧
      psiFiveCoreAnalog (20 * n + 5) = -fiveCoreCount (5 * n + 1) ∧
      2 * psiFiveCoreAnalog (20 * n + 7) =
        phiFiveCoreAnalog (2 * n + 1) + 2 * fiveCoreCount (2 * n) ∧
      psiFiveCoreAnalog (20 * n + 9) = -fiveCoreCount (5 * n + 2) ∧
      psiFiveCoreAnalog (20 * n + 15) = 0 ∧
      psiFiveCoreAnalog (20 * n + 19) = 0
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Theorem 5 (jis-2024-24.4.5-thm-5).
Uses 3
Statement usesThe 5-core counts · The φ-analog of the 5-core partition function · The ψ-analog of the 5-core partition function

TheoremSign densities of the ψ-analog of the 5-core partition function#●ready to prove

Let \(\bar b_5(n)\) be the coefficient of \(q^n\) in \(\psi^5(-q^5)/\psi(-q)\), where \(\psi(q) = \sum_{n \ge 0} q^{n(n+1)/2}\), and let the lower density of a set \(S\) of natural numbers be \(\liminf_{N \to \infty} |S \cap \{0, \dots, N - 1\}|/N\). The set of positive integers \(n\) with \(\bar b_5(n) = 0\) has lower density at least \(3/10\), the set of positive \(n\) with \(\bar b_5(n) > 0\) has lower density at least \(52/100\), and the set of positive \(n\) with \(\bar b_5(n) < 0\) has lower density at least \(1/10\).

public theorem_wanted psiFiveCoreAnalog_sign_densities :
    3 / 10 ≤ {n : ℕ | 0 < n ∧ psiFiveCoreAnalog n = 0}.lowerDensity ∧
      52 / 100 ≤ {n : ℕ | 0 < n ∧ 0 < psiFiveCoreAnalog n}.lowerDensity ∧
      1 / 10 ≤ {n : ℕ | 0 < n ∧ psiFiveCoreAnalog n < 0}.lowerDensity
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Corollary 6 (jis-2024-24.4.5-cor-6).
Uses 2
Statement usesThe ψ-analog of the 5-core partition function · Lower density

TheoremThe \(\varphi\)-analog in terms of the \(\psi\)-analog of the 5-core counts#●ready to prove

Let \(\varphi(q) = \sum_{n \in \mathbb{Z}} q^{n^2}\) and \(\psi(q) = \sum_{n \in \mathbb{Z}} q^{n(2n-1)}\), and let \(\bar a_5(n)\) and \(\bar b_5(n)\) be the coefficients of \(q^n\) in \(\varphi(-q^5)^5 / \varphi(-q)\) and \(\psi(-q^5)^5 / \psi(-q)\) respectively. For every natural number \(n\), \(\bar a_5(20n+6) = 20\, \bar b_5(10n)\) and \(\bar a_5(20n+14) = 20\, \bar b_5(10n+4)\).

public theorem_wanted phiFiveCoreAnalog_eq_twenty_mul_psiFiveCoreAnalog (n : ℕ) :
    phiFiveCoreAnalog (20 * n + 6) = 20 * psiFiveCoreAnalog (10 * n) ∧
      phiFiveCoreAnalog (20 * n + 14) = 20 * psiFiveCoreAnalog (10 * n + 4)
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Corollary 7 (jis-2024-24.4.5-cor-7).
Uses 2
Statement usesThe φ-analog of the 5-core partition function · The ψ-analog of the 5-core partition function

TheoremCongruences for the ψ-analog of the 5-core partition function#●ready to prove

Let \(\bar b_5(n)\) be the coefficient of \(q^n\) in \(\psi^5(-q^5)/\psi(-q)\), where \(\psi(q) = \sum_{n \ge 0} q^{n(n+1)/2}\). For every integer \(k \ge 2\) and every natural number \(n\), \(4 \bar b_5(5^k(n+3) - 3) \equiv 5 \bar b_5(n) - \bar b_5(5n+12) \pmod{5^k}\), and both \(\bar b_5(5^k(20n+18) - 3)\) and \(\bar b_5(5^k(20n+22) - 3)\) are divisible by \((5^k - 1)/4\).

public theorem_wanted psiFiveCoreAnalog_congruences {k : ℕ} (hk : 2 ≤ k) (n : ℕ) :
    4 * psiFiveCoreAnalog (5 ^ k * (n + 3) - 3) ≡
        5 * psiFiveCoreAnalog n - psiFiveCoreAnalog (5 * n + 12) [ZMOD 5 ^ k] ∧
      psiFiveCoreAnalog (5 ^ k * (20 * n + 18) - 3) ≡ 0 [ZMOD (5 ^ k - 1) / 4] ∧
      psiFiveCoreAnalog (5 ^ k * (20 * n + 22) - 3) ≡ 0 [ZMOD (5 ^ k - 1) / 4]
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Corollary 8 (jis-2024-24.4.5-cor-8).
Uses 1
Statement usesThe ψ-analog of the 5-core partition function

TheoremTheta-function identities of level 5#●ready to prove

Let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), \(f(q) = \prod_{m \ge 1} (1 - (-q)^m)\) (so that \(f(-q) = f_1\)), \(\chi(-q) = \prod_{m \ge 0} (1 - q^{2m+1})\) and \(\chi(q) = \prod_{m \ge 0} (1 + q^{2m+1})\). Let \(f(a, b) = \sum_{n \in \mathbb{Z}} a^{n(n+1)/2} b^{n(n-1)/2}\) be Ramanujan's general theta function, \(\varphi(q) = f(q, q)\) and \(\psi(q) = f(q, q^3)\). Then, as integer power series in \(q\) (every denominator below has constant term \(1\)): \(\varphi^5(q^5)/\varphi(q) + 4q f^5(q^5)/f(q) = \varphi(q) \varphi^3(q^5)\); \(\varphi^2(q) - \varphi^2(q^5) = 4q \chi(q) f_5 f_{20}\); \(\psi^5(-q^5)/\psi(-q) - \psi^5(q^5)/\psi(q) = 4q^3 \psi^5(q^{10})/\psi(q^2) + 2q f_{20}^5/f_4\); \(\psi^2(q) - q \psi^2(q^5) = f_5 \varphi(-q^5)/\chi(-q) = f(q, q^4) f(q^2, q^3)\); \(f_5^5/f_1 - 4q^3 f_{20}^5/f_4 = f^5(q^5)/f(q) + 2q f_{10}^5/f_2\); and \(f_2^2/f_1^4 = f_{10}^2/f_5^4 + 4q f_2 f_{10}^5/(f_1^3 f_5^5)\).

MetaMathlibExt.theta_level_five_identities · 18 lines 
public theorem_wanted theta_level_five_identities :
    expand 5 (by norm_num) Φ ^ 5 * rescale (-1) (𝔣 1) +
        4 * X * expand 5 (by norm_num) (rescale (-1) (𝔣 1)) ^ 5 * Φ =
      Φ ^ 2 * expand 5 (by norm_num) Φ ^ 3 * rescale (-1) (𝔣 1) ∧
    Φ ^ 2 - expand 5 (by norm_num) Φ ^ 2 =
      4 * X * rescale (-1) (∏' m : ℕ, (1 - X ^ (2 * m + 1)) : ℤ⟦X⟧) * 𝔣 5 * 𝔣 20 ∧
    expand 5 (by norm_num) (rescale (-1) Ψ) ^ 5 * Ψ * expand 2 (by norm_num) Ψ * 𝔣 4 -
        expand 5 (by norm_num) Ψ ^ 5 * rescale (-1) Ψ * expand 2 (by norm_num) Ψ * 𝔣 4 =
      4 * X ^ 3 * expand 10 (by norm_num) Ψ ^ 5 * rescale (-1) Ψ * Ψ * 𝔣 4 +
        2 * X * 𝔣 20 ^ 5 * rescale (-1) Ψ * Ψ * expand 2 (by norm_num) Ψ ∧
    (Ψ ^ 2 - X * expand 5 (by norm_num) Ψ ^ 2) * (∏' m : ℕ, (1 - X ^ (2 * m + 1)) : ℤ⟦X⟧) =
      𝔣 5 * expand 5 (by norm_num) (rescale (-1) Φ) ∧
    Ψ ^ 2 - X * expand 5 (by norm_num) Ψ ^ 2 = ramanujanThetaPow 1 4 * ramanujanThetaPow 2 3 ∧
    𝔣 5 ^ 5 * 𝔣 4 * rescale (-1) (𝔣 1) * 𝔣 2 -
        4 * X ^ 3 * 𝔣 20 ^ 5 * 𝔣 1 * rescale (-1) (𝔣 1) * 𝔣 2 =
      expand 5 (by norm_num) (rescale (-1) (𝔣 1)) ^ 5 * 𝔣 1 * 𝔣 4 * 𝔣 2 +
        2 * X * 𝔣 10 ^ 5 * 𝔣 1 * 𝔣 4 * rescale (-1) (𝔣 1) ∧
    𝔣 2 ^ 2 * 𝔣 5 ^ 5 = 𝔣 10 ^ 2 * 𝔣 5 * 𝔣 1 ^ 4 + 4 * X * 𝔣 2 * 𝔣 10 ^ 5 * 𝔣 1
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Lemma 9 (jis-2024-24.4.5-lem-9).
Uses 2
Statement usesThe Euler products of partition theory · Ramanujan's general theta function at powers of q

Theorem5-dissections of Ramanujan's theta functions φ and ψ#●ready to prove

Let \(f(a, b) = \sum_{n \in \mathbb{Z}} a^{n(n+1)/2} b^{n(n-1)/2}\) be Ramanujan's general theta function, \(\varphi(q) = f(q, q)\) and \(\psi(q) = f(q, q^3)\). As integer power series in \(q\), \(\varphi(q) = \varphi(q^{25}) + 2q f(q^{15}, q^{35}) + 2q^4 f(q^5, q^{45})\) and \(\psi(q) = f(q^{10}, q^{15}) + q f(q^5, q^{20}) + q^3 \psi(q^{25})\).

Lemma 10 of the source also gives a 5-dissection of \(\prod_{m \ge 1} (1 - q^m)^{-1}\) via the Rogers–Ramanujan continued fraction; that part is not included.

public theorem_wanted theta_five_dissections :
    Φ = expand 25 (by norm_num) Φ + 2 * X * ramanujanThetaPow 15 35 +
        2 * X ^ 4 * ramanujanThetaPow 5 45 ∧
      Ψ = ramanujanThetaPow 10 15 + X * ramanujanThetaPow 5 20 + X ^ 3 * expand 25 (by norm_num) Ψ
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Lemma 10 (jis-2024-24.4.5-lem-10).
Uses 1
Statement usesRamanujan's general theta function at powers of q

TheoremTwo identities for the 5-core counts#●ready to prove

Let \(f_k = \prod_{m \ge 1} (1 - q^{km})\) and let \(c_5(n)\) be the coefficient of \(q^n\) in \(f_5^5 / f_1\). For every natural number \(n\), \(c_5(4n+1) = c_5(2n)\) and \(c_5(5n+4) = 5\, c_5(n)\).

public theorem_wanted fiveCoreCount_identities (n : ℕ) :
    fiveCoreCount (4 * n + 1) = fiveCoreCount (2 * n) ∧
      fiveCoreCount (5 * n + 4) = 5 * fiveCoreCount n
Sources
  • Subhajit Bandyopadhyay and Nayandeep Deka Baruah, Arithmetic Identities for Some Analogs of the 5-Core Partition Function, Journal of Integer Sequences 27 (2024), Article 24.4.5, Lemma 11 (jis-2024-24.4.5-lem-11).
Uses 1
Statement usesThe 5-core counts
8 fully proved12 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.