Dold and realizable sequences

DefinitionBinomial-power sequences#✓fully proved

For natural numbers \(r\), \(s\) and \(n\), the binomial-power number \(A_{r,s}(n)\) is the natural number

\[A_{r,s}(n) = \sum_{k=0}^{n} \binom{n}{k}^r \binom{n+k}{k}^s.\]

Special cases include the central Delannoy numbers (\(r = s = 1\)), the Apéry numbers (\(r = s = 2\)) and the Franel numbers of order \(r\) (\(s = 0\)).

def binomialPowerSeq (r s n : ℕ) : ℕ :=
  ∑ k ∈ Finset.range (n + 1),
    (Nat.choose n k) ^ r * (Nat.choose (n + k) k) ^ s
Sources
  • Geng-Rui Zhang, "Realizability of Some Combinatorial Sequences," Journal of Integer Sequences 27 (2024), Article 24.3.3, Theorem, lines 143–144, https://cs.uwaterloo.ca/journals/JIS/VOL27/Zhang/zhang9.tex with A(n,r,s) at lines 120–122 and realizability at lines 86–93.
Used by 7
Used byA binomial sum through central Delannoy numbers · Dold congruences for binomial-power sequences · Non-negativity of the Möbius transform of binomial-power sequences · Binomial-power sequences are Dold realizable · Binomial-power sequences are almost realizable · Explicit formula for A265233 in terms of Franel numbers · Franel numbers as diagonal coefficients

DefinitionDold realizable sequences#✓fully proved

An integer sequence \((a(n))_{n \ge 0}\) is Dold realizable when, for every integer \(n \ge 1\), the Möbius transform \(\sum_{d \mid n} \mu(d)\, a(n/d)\) is divisible by \(n\) and non-negative, where \(\mu\) is the Möbius function and \(d\) runs over the positive divisors of \(n\).

The divisibility condition alone is the classical Dold condition.

def doldRealizable (a : ℕ → ℤ) : Prop :=
  ∀ n : ℕ, 0 < n →
    (n : ℤ) ∣ ∑ d ∈ Nat.divisors n,
      (⇑ArithmeticFunction.moebius d) * a (n / d) ∧
    0 ≤ ∑ d ∈ Nat.divisors n,
      (⇑ArithmeticFunction.moebius d) * a (n / d)
Sources
  • Wójcik, Lemma 3, for an equivalent form of the Dold condition.
Used by 9
Used byBinomial-power sequences are Dold realizable · Domb-type sums are Dold realizable · Dold realizable sequences satisfy the Dold congruences · Even-binomial-type sums are Dold realizable · The Möbius transform of a Dold realizable sequence is non-negative · Criterion for Dold realizability · Almost realizable sequences · Binomial-power sequences are almost realizable · The zero sequence is almost realizable

TheoremDold realizable sequences satisfy the Dold congruences#✓fully proved

If an integer sequence \((a(n))_{n \ge 0}\) is Dold realizable, then for every integer \(n \ge 1\), \(n\) divides \(\sum_{d \mid n} \mu(d)\, a(n/d)\), where \(\mu\) is the Möbius function and \(d\) runs over the positive divisors of \(n\).

theorem doldRealizable_dvd {a : ℕ → ℤ} (h : doldRealizable a) (n : ℕ)
    (hn : 0 < n) :
    (n : ℤ) ∣ ∑ d ∈ Nat.divisors n,
      (⇑ArithmeticFunction.moebius d) * a (n / d)
Uses 1 · Used by 1
Statement usesDold realizable sequences
Used byDold congruences for binomial-power sequences

TheoremThe Möbius transform of a Dold realizable sequence is non-negative#✓fully proved

If an integer sequence \((a(n))_{n \ge 0}\) is Dold realizable, then for every integer \(n \ge 1\), \(\sum_{d \mid n} \mu(d)\, a(n/d) \ge 0\), where \(\mu\) is the Möbius function and \(d\) runs over the positive divisors of \(n\).

theorem doldRealizable_nonneg {a : ℕ → ℤ} (h : doldRealizable a) (n : ℕ)
    (hn : 0 < n) :
    0 ≤ ∑ d ∈ Nat.divisors n,
      (⇑ArithmeticFunction.moebius d) * a (n / d)
Uses 1 · Used by 1
Statement usesDold realizable sequences
Used byNon-negativity of the Möbius transform of binomial-power sequences

TheoremCriterion for Dold realizability#✓fully proved

Let \((a(n))_{n \ge 0}\) be an integer sequence and let \(\mu\) be the Möbius function. If for every integer \(n \ge 1\) the sum \(\sum_{d \mid n} \mu(d)\, a(n/d)\) over the positive divisors \(d\) of \(n\) is divisible by \(n\), and for every integer \(n \ge 1\) this sum is non-negative, then \(a\) is Dold realizable.

theorem doldRealizable_of_dvd_and_nonneg {a : ℕ → ℤ}
    (hdvd : ∀ n : ℕ, 0 < n →
      (n : ℤ) ∣ ∑ d ∈ Nat.divisors n,
        (⇑ArithmeticFunction.moebius d) * a (n / d))
    (hnn : ∀ n : ℕ, 0 < n →
      0 ≤ ∑ d ∈ Nat.divisors n,
        (⇑ArithmeticFunction.moebius d) * a (n / d)) :
    doldRealizable a
Uses 1
Statement usesDold realizable sequences

TheoremBinomial-power sequences are Dold realizable#✓fully proved

Let \(r \ge 1\) and \(s \ge 0\) be integers and let \(A_{r,s}(n) = \sum_{k=0}^{n} \binom{n}{k}^r \binom{n+k}{k}^s\). Then the integer sequence \((A_{r,s}(n))_{n \ge 0}\) is Dold realizable: for every integer \(n \ge 1\), the sum \(\sum_{d \mid n} \mu(d)\, A_{r,s}(n/d)\) over the positive divisors \(d\) of \(n\), where \(\mu\) is the Möbius function, is non-negative and divisible by \(n\).

theorem binomial_power_sequence_dold_realizable : ∀ r s : ℕ, 0 < r → doldRealizable
  (fun n => ((binomialPowerSeq r s n : ℕ) : ℤ))
Sources
  • Zhang 2024, J. Integer Seq. 27, Article 24.3.3, Theorem 1.13.
Uses 2 · Used by 3
Statement usesBinomial-power sequences · Dold realizable sequences
Used byDold congruences for binomial-power sequences · Non-negativity of the Möbius transform of binomial-power sequences · Binomial-power sequences are almost realizable

TheoremDold congruences for binomial-power sequences#✓fully proved

Let \(r \ge 1\) and \(s \ge 0\) be integers and let \(A_{r,s}(m) = \sum_{k=0}^{m} \binom{m}{k}^r \binom{m+k}{k}^s\). Then for every integer \(n \ge 1\), \(n\) divides \(\sum_{d \mid n} \mu(d)\, A_{r,s}(n/d)\), where \(\mu\) is the Möbius function and \(d\) runs over the positive divisors of \(n\).

theorem binomialPowerSeq_dold_congruences (r s : ℕ) (hr : 0 < r) (n : ℕ)
    (hn : 0 < n) :
    (n : ℤ) ∣ ∑ d ∈ Nat.divisors n, (⇑ArithmeticFunction.moebius d) *
      ((binomialPowerSeq r s (n / d) : ℕ) : ℤ)
Uses 3
Statement usesBinomial-power sequences
Proof usesBinomial-power sequences are Dold realizable · Dold realizable sequences satisfy the Dold congruences

TheoremNon-negativity of the Möbius transform of binomial-power sequences#✓fully proved

Let \(r \ge 1\) and \(s \ge 0\) be integers and let \(A_{r,s}(m) = \sum_{k=0}^{m} \binom{m}{k}^r \binom{m+k}{k}^s\). Then for every integer \(n \ge 1\), \(\sum_{d \mid n} \mu(d)\, A_{r,s}(n/d) \ge 0\), where \(\mu\) is the Möbius function and \(d\) runs over the positive divisors of \(n\).

theorem binomialPowerSeq_moebius_sum_nonneg (r s : ℕ) (hr : 0 < r) (n : ℕ)
    (hn : 0 < n) :
    0 ≤ ∑ d ∈ Nat.divisors n, (⇑ArithmeticFunction.moebius d) *
      ((binomialPowerSeq r s (n / d) : ℕ) : ℤ)
Uses 3
Statement usesBinomial-power sequences
Proof usesBinomial-power sequences are Dold realizable · The Möbius transform of a Dold realizable sequence is non-negative

DefinitionDold sequences#✓fully proved

A sequence \(a_0, a_1, a_2, \dots\) of integers is a Dold sequence when for every integer \(m \ge 1\) there is an \(m \times m\) matrix \(A\) with integer entries such that \(a_n = \operatorname{tr}(A^n)\) for every \(n\) with \(1 \le n \le m\). The term \(a_0\) is not constrained.

def IsDoldSequence (a : ℕ → ℤ) : Prop :=
  ∀ m : ℕ, 1 ≤ m →
    ∃ A : Matrix (Fin m) (Fin m) ℤ,
      ∀ n : ℕ, 1 ≤ n → n ≤ m → a n = Matrix.trace (A ^ n)
Sources
  • Wójcik, Binomial Transform and Dold Sequences, Lemma 3; this equivalent trace characterization is taken here as the definition.

DefinitionFermat sequence#✓fully proved

Given a sequence \(b : \mathbb{N} \to \mathbb{C}\), the Fermat sequence generated by \(b\) is the sequence \(a : \mathbb{N} \to \mathbb{C}\) given by \(a_n = \sum_{m \mid n} m \, b_m\) for \(n \ge 1\), the sum running over the positive divisors \(m\) of \(n\), and \(a_0 = 0\).

The source defines the sequence only for positive indices; the value \(a_0 = 0\) comes from summing over the empty set of divisors of \(0\).

public def fermatSequence (b : ℕ → ℂ) : ℕ → ℂ :=
  fun n => ∑ m ∈ Nat.divisors n, (m : ℂ) * b m
Sources

DefinitionAlmost realizable sequences#✓fully proved

A sequence \(a\) of natural numbers \(a(0), a(1), \dots\) is almost realizable when there is an integer \(m \ge 1\) such that the integer sequence \((m\, a(n))_{n \ge 0}\) is Dold realizable: for every \(n \ge 1\), the sum \(\sum_{d \mid n} \mu(d)\, m\, a(n/d)\) over the positive divisors \(d\) of \(n\), where \(\mu\) is the Möbius function, is non-negative and divisible by \(n\).

This is Miska and Ward's notion that some positive integer multiple of \(a\) is realizable. The value \(a(0)\) is not used.

def IsAlmostRealizableSeq (a : ℕ → ℕ) : Prop :=
  ∃ m : ℕ, 0 < m ∧ doldRealizable fun n => ((m * a n : ℕ) : ℤ)
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Definition 3.
Uses 1 · Used by 3
Statement usesDold realizable sequences
Used byBinomial-power sequences are almost realizable · The zero sequence is almost realizable · The Catalan, Motzkin and large Schröder numbers are not almost realizable

TheoremThe zero sequence is almost realizable#✓fully proved

The constant sequence \(a(n) = 0\) is almost realizable.

It is realized by the self-map of the empty set, with multiplier \(m = 1\).

theorem isAlmostRealizableSeq_zero : IsAlmostRealizableSeq fun _ => 0
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Definition 3.
Uses 2
Statement usesAlmost realizable sequences
Proof usesDold realizable sequences

TheoremBinomial-power sequences are almost realizable#✓fully proved

For all natural numbers \(r \ge 1\) and \(s\), the binomial-power sequence \(n \mapsto \sum_{k=0}^{n} \binom{n}{k}^r \binom{n+k}{k}^s\) is almost realizable.

Every Dold realizable sequence is almost realizable (take the multiplier \(m = 1\)), and the binomial-power sequences are Dold realizable.

theorem isAlmostRealizableSeq_binomialPowerSeq (r s : ℕ) (hr : 0 < r) :
    IsAlmostRealizableSeq fun n => binomialPowerSeq r s n
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Definition 3 and Theorem 13.
Uses 4
Statement usesAlmost realizable sequences · Binomial-power sequences
Proof usesBinomial-power sequences are Dold realizable · Dold realizable sequences

TheoremDomb-type sums are Dold realizable#●ready to prove

For all natural numbers \(r \ge 1\), \(s\) and \(t\), the integer sequence \((D(n, r, s, t))_{n \ge 0}\) of Domb-type sums \(D(n, r, s, t) = \sum_{k=0}^{n} \binom{n}{k}^r \binom{2k}{k}^s \binom{2(n-k)}{n-k}^t\) is Dold realizable.

public theorem_wanted doldRealizable_dombTypeSum (r s t : ℕ) (hr : 1 ≤ r) :
    doldRealizable fun n => ((dombTypeSum n r s t : ℕ) : ℤ)
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Theorem 15 (jis-2024-24.3.3-thm-15).
Uses 2
Statement usesDold realizable sequences · Domb-type sums

TheoremThe Catalan, Motzkin and large Schröder numbers are not almost realizable#●ready to prove

None of the following three sequences of non-negative integers is almost realizable: the Catalan numbers \(C_n = \frac{1}{n+1}\binom{2n}{n}\), the Motzkin numbers \(M(n)\), and the large Schröder numbers \(S(n)\) (OEIS A006318), given by \(S(0) = 1\) and \(S(n+1) = S(n) + \sum_{i=0}^{n} S(i) S(n-i)\).

public theorem_wanted not_isAlmostRealizableSeq_catalan_motzkin_schroder :
    ¬ IsAlmostRealizableSeq catalan ∧ ¬ IsAlmostRealizableSeq motzkinNumber ∧
      ¬ IsAlmostRealizableSeq Nat.largeSchroder
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Theorem 21 (jis-2024-24.3.3-thm-21).
Uses 2
Statement usesAlmost realizable sequences · Motzkin numbers as a Catalan-weighted binomial sum

TheoremHelou–Terjanian congruence for primes \(p \ge 5\)#●ready to prove

Let \(p \ge 5\) be a prime and let \(m\) and \(n\) be integers with \(0 < m < n\). Then \(\binom{np}{mp} \equiv \binom{n}{m} \pmod{p^e}\), where \(e = 3 + \max(\nu_p(m), \nu_p(n - m)) + \nu_p\big(\binom{n}{m}\big)\) and \(\nu_p\) is the \(p\)-adic valuation.

public theorem_wanted choose_mul_prime_modEq_of_five_le (p n m : ℕ) (hp : p.Prime) (hp5 : 5 ≤ p)
    (hm : 0 < m) (hmn : m < n) :
    (n * p).choose (m * p) ≡ n.choose m
      [MOD p ^ (3 + max (padicValNat p m) (padicValNat p (n - m)) +
        padicValNat p (n.choose m))]
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Lemma 26 (1) (jis-2024-24.3.3-lem-26).

TheoremHelou–Terjanian congruence for \(p = 3\)#●ready to prove

Let \(m\) and \(n\) be integers with \(0 < m < n\). Then \(\binom{3n}{3m} \equiv \binom{n}{m} \pmod{3^e}\), where \(e = 2 + \max(\nu_3(m), \nu_3(n - m)) + \nu_3\big(\binom{n}{m}\big)\) and \(\nu_3\) is the \(3\)-adic valuation.

public theorem_wanted choose_three_mul_modEq (n m : ℕ) (hm : 0 < m) (hmn : m < n) :
    (3 * n).choose (3 * m) ≡ n.choose m
      [MOD 3 ^ (2 + max (padicValNat 3 m) (padicValNat 3 (n - m)) +
        padicValNat 3 (n.choose m))]
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Lemma 26 (2) (jis-2024-24.3.3-lem-26).

TheoremHelou–Terjanian congruence for \(p = 2\)#●ready to prove

Let \(m\) and \(n\) be integers with \(0 < m < n\). Then \(\binom{2n}{2m} \equiv \binom{n}{m} \pmod{2^e}\), where \(e = 1 + \max(\nu_2(m), \nu_2(n - m)) + \nu_2\big(\binom{n}{m}\big)\) and \(\nu_2\) is the \(2\)-adic valuation.

public theorem_wanted choose_two_mul_modEq (n m : ℕ) (hm : 0 < m) (hmn : m < n) :
    (2 * n).choose (2 * m) ≡ n.choose m
      [MOD 2 ^ (1 + max (padicValNat 2 m) (padicValNat 2 (n - m)) +
        padicValNat 2 (n.choose m))]
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Lemma 26 (3) (jis-2024-24.3.3-lem-26).

TheoremBinomial coefficients at multiples of a prime divisor#●ready to prove

Let \(p\) be a prime and let \(n \ge 1\) be an integer divisible by \(p\). Then for every integer \(\lambda \ge 0\) with \(\lambda p \ne n\),

\[\binom{n}{\lambda p} \equiv \binom{n/p}{\lambda} \pmod{p^e},\]

where \(e = \max(\nu_p(n), \nu_p(n - \lambda p))\) and \(\nu_p\) is the \(p\)-adic valuation; the integer \(n - \lambda p\) may be negative, and \(\nu_p(n - \lambda p)\) is the valuation of its absolute value.

public theorem_wanted choose_mul_prime_modEq_choose_div (n p l : ℕ) (hp : p.Prime) (hpn : p ∣ n)
    (hn : 0 < n) (hl : l * p ≠ n) :
    (n.choose (l * p) : ℤ) ≡ ((n / p).choose l : ℤ)
      [ZMOD (p : ℤ) ^ max (padicValNat p n) (padicValInt p ((n : ℤ) - l * p))]
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Lemma 27 (jis-2024-24.3.3-lem-27).

TheoremMöbius transforms of sequences growing by a factor of at least \(1.221\) are nonnegative#●ready to prove

Let \(b\) be a sequence of real numbers and \(C \ge 1.221\) a real number such that \(b(n) \ge 0\) and \(b(n+1) \ge C\, b(n)\) for every \(n \ge 1\). Then for every \(n \ge 1\), with \(\mu\) the Möbius function,

\[\sum_{d \mid n} \mu(n/d)\, b(d) \ge 0,\]

that is, the Dirichlet convolution \(\mu * b\) is nonnegative at \(n\).

public theorem_wanted moebius_conv_nonneg_of_geometric_growth (b : ℕ → ℝ)
    (hb : ∀ n, 1 ≤ n → 0 ≤ b n) (C : ℝ) (hC : (1221 / 1000 : ℝ) ≤ C)
    (hgrowth : ∀ n, 1 ≤ n → C * b n ≤ b (n + 1)) (n : ℕ) (hn : 1 ≤ n) :
    0 ≤ ∑ d ∈ n.divisors, (ArithmeticFunction.moebius (n / d) : ℝ) * b d
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Lemma 28 (jis-2024-24.3.3-lem-28).

TheoremDold congruences via prime-power congruences#●ready to prove

Let \((V(n))_{n \ge 1}\) be a sequence of integers and let \(\mu\) denote the Möbius function. Then \(V(n p^m) \equiv V(n p^{m-1}) \pmod{p^m}\) holds for all integers \(n, m \ge 1\) and all primes \(p\) if and only if \(n\) divides \(\sum_{d \mid n} \mu(n/d) V(d)\) for every integer \(n \ge 1\).

public theorem_wanted prime_power_congruence_iff_dold (V : ℕ → ℤ) :
    (∀ n m p : ℕ, 1 ≤ n → 1 ≤ m → p.Prime →
        V (n * p ^ m) ≡ V (n * p ^ (m - 1)) [ZMOD (p : ℤ) ^ m]) ↔
      ∀ n : ℕ, 1 ≤ n →
        (n : ℤ) ∣ ∑ d ∈ n.divisors, (ArithmeticFunction.moebius (n / d) : ℤ) * V d
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Lemma 30 (jis-2024-24.3.3-lem-30).

TheoremEven-binomial-type sums are Dold realizable#●ready to prove

Let \(r \ge 1\), \(s\), \(t\) and \(u\) be natural numbers with \(t + u \ge 1\), and let

\[T(n) = \sum_{k=0}^{n} \binom{n}{2k}^r \binom{n+k}{k}^s \binom{2k}{k}^t \binom{2(n-k)}{n-k}^u.\]

Then the integer sequence \((T(n))_{n \ge 0}\) is Dold realizable.

The hypothesis \(t + u \ge 1\) is added to the source: for \(t = u = 0\) the Möbius transform at \(n = 2\) is \(T(2) - T(1) = 3^s\), which is odd, so the sequence is not Dold realizable.

public theorem_wanted doldRealizable_evenBinomialTypeSum (r s t u : ℕ) (hr : 1 ≤ r)
    (htu : 1 ≤ t + u) :
    doldRealizable fun n => ((∑ k ∈ Finset.range (n + 1),
      n.choose (2 * k) ^ r * (n + k).choose k ^ s * (2 * k).choose k ^ t *
        (2 * (n - k)).choose (n - k) ^ u : ℕ) : ℤ)
Sources
  • Geng-Rui Zhang, Realizability of Some Combinatorial Sequences, Journal of Integer Sequences 27 (2024), Article 24.3.3, Theorem 18 (jis-2024-24.3.3-thm-18).
Uses 1
Statement usesDold realizable sequences
13 fully proved9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.