Mex-related partition functions

TheoremLifting partition congruences to mex partition functions#✓fully proved

For a partition \(\lambda\), a positive integer \(A\) and a natural number \(c\), let \(\operatorname{mex}_{A,c}(\lambda)\) be the smallest positive integer congruent to \(c\) modulo \(A\) that is not a part of \(\lambda\), and let \(p_{A,c}(N)\) be the number of partitions \(\lambda\) of \(N\) with \(\operatorname{mex}_{A,c}(\lambda) \equiv c \pmod{2A}\). Let \(p(N)\) be the number of partitions of \(N\). Let \(m\), \(a\) and \(b\) be natural numbers with \(m \ge 1\) and \(b < a\), and suppose that \(m\) divides \(p(an + b)\) for every natural number \(n\). Then for every integer \(t \ge 1\) and every natural number \(n\), \(m\) divides both \(p_{at,at}(an + b)\) and \(p_{2at,at}(an + b)\).

Because \(b < a\), the hypothesis covers the whole residue class of \(b\) modulo \(a\); for \(b \ge a\) the lift would need \(p\) at arguments below \(b\), which the hypothesis does not cover.

The proof follows the Andrews–Newman mex decomposition used by Barman and Singh: remove one copy of every forced earlier mex candidate. The exact-mex fibers then telescope, while every removed prefix sum remains a multiple of \(a\).

MetaMathlibExt.mesh_partition_congruence_lift · 18 lines 
public theorem mesh_partition_congruence_lift
    (m a b : ℕ) (_hm : 0 < m) (ha : 0 < a) (hb : b < a)
    (hbase : ∀ n : ℕ, m ∣ Fintype.card (Nat.Partition (a * n + b))) :
    ∀ t : ℕ, 0 < t →
      (∀ n : ℕ, m ∣ (@Finset.filter (Nat.Partition (a * n + b))
        (fun lam => ∃ μ : ℕ, 0 < μ ∧ μ % (a * t) = (a * t) % (a * t) ∧
          μ ∉ lam.parts ∧
          (∀ k : ℕ, 0 < k → k < μ → k % (a * t) = (a * t) % (a * t) →
            k ∈ lam.parts) ∧
          μ % (2 * (a * t)) = (a * t) % (2 * (a * t)))
        (Classical.decPred _) Finset.univ).card) ∧
      (∀ n : ℕ, m ∣ (@Finset.filter (Nat.Partition (a * n + b))
        (fun lam => ∃ μ : ℕ, 0 < μ ∧ μ % (2 * a * t) = (a * t) % (2 * a * t) ∧
          μ ∉ lam.parts ∧
          (∀ k : ℕ, 0 < k → k < μ → k % (2 * a * t) = (a * t) % (2 * a * t) →
            k ∈ lam.parts) ∧
          μ % (2 * (2 * a * t)) = (a * t) % (2 * (2 * a * t)))
        (Classical.decPred _) Finset.univ).card)
Sources
  • Rupam Barman and Ajit Singh, "Mex-Related Partition Functions of Andrews and Newman," Journal of Integer Sequences 24 (2021), Article 21.6.3, Theorem, lines 172–182, https://cs.uwaterloo.ca/journals/JIS/VOL24/Barman/barman3.tex

DefinitionMex of a partition in a residue class#✓fully proved

For natural numbers \(A\), \(a\) and \(n\) and a partition \(\lambda\) of \(n\), \(\operatorname{mex}_{A,a}(\lambda)\) is the smallest positive integer congruent to \(a\) modulo \(A\) that is not a part of \(\lambda\), and \(0\) if there is no such integer (which happens only when \(A = 0\)).

noncomputable def partitionMex (A a : ℕ) {n : ℕ} (lam : Nat.Partition n) : ℕ :=
  sInf { m : ℕ | 0 < m ∧ m ≡ a [MOD A] ∧ m ∉ lam.parts }
Used by 1
Used byMex-related partition function of Andrews and Newman

DefinitionMex-related partition function of Andrews and Newman#✓fully proved

For natural numbers \(A\), \(a\) and \(n\), \(p_{A,a}(n)\) is the number of partitions \(\lambda\) of \(n\) such that \(\operatorname{mex}_{A,a}(\lambda) \equiv a \pmod{2A}\), where \(\operatorname{mex}_{A,a}(\lambda)\) is the smallest positive integer congruent to \(a\) modulo \(A\) that is not a part of \(\lambda\), and \(0\) if there is no such integer.

noncomputable def mexPartitionNumber (A a n : ℕ) : ℕ := by
  classical
  exact ((Finset.univ : Finset (Nat.Partition n)).filter
    (fun lam => decide (partitionMex A a lam ≡ a [MOD 2 * A]))).card
Uses 1 · Used by 1
Statement usesMex of a partition in a residue class
Used byRamanujan congruences for mex-related partition functions

DefinitionLeast inverse of 24 modulo a power#✓fully proved

For natural numbers \(p\) and \(k\), \(\delta_{p,k}\) is the least natural number \(\delta\) with \(24\delta \equiv 1 \pmod{p^k}\), and \(0\) if there is no such \(\delta\), which happens exactly when \(p^k\) and \(24\) have a common factor greater than \(1\).

noncomputable def ramanujanDelta (p k : ℕ) : ℕ :=
  sInf { delta : ℕ | 24 * delta ≡ 1 [MOD p ^ k] }
Used by 1
Used byRamanujan congruences for mex-related partition functions

TheoremRamanujan congruences for mex-related partition functions#●ready to prove

For a positive integer \(A\), a natural number \(a\) and a partition \(\lambda\), let \(\operatorname{mex}_{A,a}(\lambda)\) be the smallest positive integer congruent to \(a\) modulo \(A\) that is not a part of \(\lambda\); let \(p_{A,a}(N)\) be the number of partitions \(\lambda\) of \(N\) with \(\operatorname{mex}_{A,a}(\lambda) \equiv a \pmod{2A}\); and let \(\delta_{p,k}\) be the least natural number \(\delta\) with \(24\delta \equiv 1 \pmod{p^k}\). Then for all natural numbers \(k \ge 1\), \(t \ge 1\) and \(n\), for each \(p \in \{5, 7, 11\}\) and for both \(A = p^k t\) and \(A = 2p^k t\),

\[p_{A,\,p^k t}(p^k n + \delta_{p,k}) \equiv 0 \pmod{p^{e}},\]

where \(e = k\) for \(p = 5\) and \(p = 11\), and \(e = \lfloor k/2 \rfloor + 1\) for \(p = 7\).

public theorem_wanted ramanujan_mex_partition_congruences
    (k t n : ℕ) (hk : 1 ≤ k) (ht : 1 ≤ t) :
    mexPartitionNumber (5 ^ k * t) (5 ^ k * t) (5 ^ k * n + ramanujanDelta 5 k) ≡
      0 [MOD 5 ^ k] ∧
    mexPartitionNumber (7 ^ k * t) (7 ^ k * t) (7 ^ k * n + ramanujanDelta 7 k) ≡
      0 [MOD 7 ^ (k / 2 + 1)] ∧
    mexPartitionNumber (11 ^ k * t) (11 ^ k * t)
      (11 ^ k * n + ramanujanDelta 11 k) ≡ 0 [MOD 11 ^ k] ∧
    mexPartitionNumber (2 * (5 ^ k * t)) (5 ^ k * t)
      (5 ^ k * n + ramanujanDelta 5 k) ≡ 0 [MOD 5 ^ k] ∧
    mexPartitionNumber (2 * (7 ^ k * t)) (7 ^ k * t)
      (7 ^ k * n + ramanujanDelta 7 k) ≡ 0 [MOD 7 ^ (k / 2 + 1)] ∧
    mexPartitionNumber (2 * (11 ^ k * t)) (11 ^ k * t)
      (11 ^ k * n + ramanujanDelta 11 k) ≡ 0 [MOD 11 ^ k]
Sources
  • Barman–Singh, JIS 24 (2021), Art. 21.6.3, corollary.
Uses 2
Statement usesMex-related partition function of Andrews and Newman · Least inverse of 24 modulo a power
4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.