Exact covering systems

DefinitionMultiplicity of an indexed system of residue classes#✓fully proved

Given \(k \in \mathbb{N}\), moduli \(m_0, \dots, m_{k-1} \in \mathbb{N}\) and residues \(r_0, \dots, r_{k-1} \in \mathbb{Z}\), the multiplicity of an integer \(z\) is the number of indices \(i < k\) with \(z \equiv r_i \pmod{m_i}\).

Indices are counted separately, so a residue class listed several times is counted that many times; a modulus \(m_i = 0\) makes the condition \(z = r_i\).

public def indexedCoverMultiplicity {k : ℕ} (moduli : Fin k → ℕ)
    (residues : Fin k → ℤ) (z : ℤ) : ℕ :=
  (Finset.univ.filter fun i => z ≡ residues i [ZMOD (moduli i : ℤ)]).card
Used by 3
Used byFraenkel's Bernoulli recurrence for exact covers by any number of classes · Fraenkel's Bernoulli recurrence for exact covers · Exact covers by residue classes

DefinitionExact covers by residue classes#✓fully proved

Let \(k \in \mathbb{N}\), let \(m_0, \dots, m_{k-1} \in \mathbb{N}\) be moduli and \(r_0, \dots, r_{k-1} \in \mathbb{Z}\) residues, and let \(M \in \mathbb{N}\) and \(T \subseteq \mathbb{Z}\). The system of residue classes \(r_i \bmod m_i\) is an exact \(M\)-cover of \(T\) when \(k \ge 2\), every \(m_i\) is positive, every \(z \in T\) satisfies \(z \equiv r_i \pmod{m_i}\) for exactly \(M\) indices \(i < k\), and every integer \(z \notin T\) satisfies \(z \equiv r_i \pmod{m_i}\) for no index \(i < k\).

Indices are counted separately, so a residue class listed several times counts that many times.

public def IsExactCoverOf {k : ℕ} (moduli : Fin k → ℕ) (residues : Fin k → ℤ)
    (M : ℕ) (target : Set ℤ) : Prop :=
  2 ≤ k ∧ (∀ i, 0 < moduli i) ∧
    (∀ z, z ∈ target → indexedCoverMultiplicity moduli residues z = M) ∧
    ∀ z, z ∉ target → indexedCoverMultiplicity moduli residues z = 0
Uses 1
Statement usesMultiplicity of an indexed system of residue classes

TheoremFraenkel's Bernoulli recurrence for exact covers by any number of classes#✓fully proved

Let \(q\), \(M\) and \(m \ge 1\) be natural numbers, and for \(i = 1, \dots, q\) let \(n_i\) be a positive integer and \(a_i\) an integer with \(0 \le a_i < n_i\). Suppose the residue classes \(a_i \bmod n_i\), counted with repetition, form an exact \(M\)-cover of \(\mathbb{Z}\): every integer \(k\) satisfies \(k \equiv a_i \pmod{n_i}\) for exactly \(M\) indices \(i\). Then

\[ B_m \Big(M - \sum_{i=1}^{q} n_i^{m-1}\Big) = \sum_{i=1}^{q} n_i^{m-1} \sum_{s=0}^{m-1} \binom{m}{s} B_s \Big(\frac{a_i}{n_i}\Big)^{m-s}, \]

where \(B_s\) is the \(s\)-th Bernoulli number, with the convention \(B_1 = -\frac{1}{2}\).

The source assumes \(q \ge 2\); the identity holds without that assumption.

theorem fraenkel_exact_M_cover_bernoulli_recurrence_general
    (q M m : ℕ) (a n : Fin q → ℕ) (hm : 1 ≤ m)
    (hn : ∀ i, 0 < n i) (ha : ∀ i, a i < n i)
    (hcover : ∀ k : ℤ, Int.indexedCoverMultiplicity n (fun i => ((a i : ℤ))) k = M) :
    bernoulli m * ((M : ℚ) - ∑ i : Fin q, ((n i : ℚ)) ^ (m - 1)) =
      ∑ i : Fin q, ((n i : ℚ)) ^ (m - 1) *
        (∑ s ∈ Finset.range m, bernoulli s * (Nat.choose m s : ℚ) *
          (((a i : ℚ)) / ((n i : ℚ))) ^ (m - s))
Uses 1 · Used by 1
Statement usesMultiplicity of an indexed system of residue classes
Used byFraenkel's Bernoulli recurrence for exact covers

TheoremFraenkel's Bernoulli recurrence for exact covers#✓fully proved

Let \(q \ge 2\), \(m \ge 1\) and \(M\) be natural numbers, and for \(i = 1, \dots, q\) let \(n_i\) be a positive integer and \(a_i\) an integer with \(0 \le a_i < n_i\). Suppose the residue classes \(a_i \bmod n_i\), counted with repetition, form an exact \(M\)-cover of \(\mathbb{Z}\): every integer \(k\) satisfies \(k \equiv a_i \pmod{n_i}\) for exactly \(M\) indices \(i\). Then

\[ B_m \Big(M - \sum_{i=1}^{q} n_i^{m-1}\Big) = \sum_{i=1}^{q} n_i^{m-1} \sum_{s=0}^{m-1} \binom{m}{s} B_s \Big(\frac{a_i}{n_i}\Big)^{m-s}, \]

where \(B_s\) is the \(s\)-th Bernoulli number, with the convention \(B_1 = -\frac{1}{2}\).

Only this direction of the source's equation (23) is stated; the converse, Beebee's variant with a parameter \(x\), and Porubsky's weighted variant are not.

theorem fraenkel_exact_M_cover_bernoulli_recurrence
    (q M m : ℕ) (a n : Fin q → ℕ)
    (hq : 2 ≤ q) (hm : 1 ≤ m)
    (hn : ∀ i, 0 < n i) (ha : ∀ i, a i < n i)
    (hcover : ∀ k : ℤ, Int.indexedCoverMultiplicity n (fun i => ((a i : ℤ))) k = M) :
    bernoulli m * ((M : ℚ) - ∑ i : Fin q, ((n i : ℚ)) ^ (m - 1)) =
      ∑ i : Fin q, ((n i : ℚ)) ^ (m - 1) *
        (∑ s ∈ Finset.range m, bernoulli s * (Nat.choose m s : ℚ) *
          (((a i : ℚ)) / ((n i : ℚ))) ^ (m - s))
Sources
Uses 2
Statement usesMultiplicity of an indexed system of residue classes
Proof usesFraenkel's Bernoulli recurrence for exact covers by any number of classes
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.