(q, r)-Whitney and Dowling numbers

Definition(q, r)-Whitney numbers of the first kind#✓fully proved

Let \(m, r, q\) be complex numbers with \(q \ne 0\), and for a natural number \(j\) let \([j]_q = \sum_{i=0}^{j-1} q^i\) be the q-integer. The (q, r)-Whitney numbers of the first kind \(w(n, k) = w_{m,r,q}(n, k)\), for natural numbers \(n\) and \(k\), are defined by \(w(0, 0) = 1\), \(w(0, k + 1) = 0\) and, for all \(n\) and \(k\),

\[w(n + 1, 0) = -q^{-n} (m [n]_q + r) \, w(n, 0),\]
\[w(n + 1, k + 1) = q^{-n} \bigl( w(n, k) - (m [n]_q + r) \, w(n, k + 1) \bigr).\]
noncomputable def whitneyFirst (m r q : ℂ) [NeZero q] : ℕ → ℕ → ℂ
  | 0 => fun | 0 => 1 | _ + 1 => 0
  | n + 1 => fun
    | 0 => (q ^ n)⁻¹ * (0 - (m * qBrack q n + r) * whitneyFirst m r q n 0)
    | k + 1 =>
      (q ^ n)⁻¹ *
        (whitneyFirst m r q n k -
          (m * qBrack q n + r) * whitneyFirst m r q n (k + 1))
Uses 1 · Used by 6

Definition(q, r)-Whitney numbers of the second kind#✓fully proved

For complex numbers \(m\), \(r\), \(q\), the \((q, r)\)-Whitney numbers of the second kind \(W_{m,r,q}(n, k)\), indexed by natural numbers \(n\) and \(k\), are defined by \(W_{m,r,q}(0, 0) = 1\), \(W_{m,r,q}(0, k + 1) = 0\), \(W_{m,r,q}(n + 1, 0) = r \, W_{m,r,q}(n, 0)\) and

\[ W_{m,r,q}(n + 1, k + 1) = q^k \, W_{m,r,q}(n, k) + (m [k + 1]_q + r) \, W_{m,r,q}(n, k + 1), \]

where \([j]_q = 1 + q + \dots + q^{j-1}\) is the \(q\)-integer.

def whitneySecond (m r q : ℂ) : ℕ → ℕ → ℂ
  | 0 => fun | 0 => 1 | _ + 1 => 0
  | n + 1 => fun
    | 0 => r * whitneySecond m r q n 0
    | k + 1 =>
      q ^ k * whitneySecond m r q n k +
        (m * qBrack q (k + 1) + r) * whitneySecond m r q n (k + 1)
Uses 1 · Used by 12

TheoremInitial value of the first-kind (q, r)-Whitney numbers#✓fully proved

For all complex numbers \(m, r, q\) with \(q \ne 0\), the (q, r)-Whitney number of the first kind satisfies \(w_{m,r,q}(0, 0) = 1\).

theorem whitneyFirst_zero_zero (m r q : ℂ) [NeZero q] : whitneyFirst m r q 0 0 = 1
Uses 1

TheoremRow zero of the first-kind (q, r)-Whitney numbers#✓fully proved

For all complex numbers \(m, r, q\) with \(q \ne 0\) and every natural number \(k\), the (q, r)-Whitney number of the first kind satisfies \(w_{m,r,q}(0, k + 1) = 0\).

theorem whitneyFirst_zero_succ (m r q : ℂ) [NeZero q] (k : ℕ) :
    whitneyFirst m r q 0 (k + 1) = 0
Uses 1 · Used by 1

TheoremColumn-zero recurrence for first-kind (q, r)-Whitney numbers#✓fully proved

Let \(m, r, q\) be complex numbers with \(q \ne 0\), write \([j]_q\) for the q-integer of \(j\), and write \(w(n, k)\) for the (q, r)-Whitney number of the first kind \(w_{m,r,q}(n, k)\). Then for every natural number \(n\),

\[w(n + 1, 0) = q^{-n} \bigl( 0 - (m [n]_q + r) \, w(n, 0) \bigr).\]

This is the general recurrence with \(w(n, -1)\) read as \(0\).

theorem whitneyFirst_succ_zero (m r q : ℂ) [NeZero q] (n : ℕ) :
    whitneyFirst m r q (n + 1) 0 =
      (q ^ n)⁻¹ * (0 - (m * qBrack q n + r) * whitneyFirst m r q n 0)
Uses 2

TheoremTriangular recurrence for first-kind (q, r)-Whitney numbers#✓fully proved

Let \(m, r, q\) be complex numbers with \(q \ne 0\), write \([j]_q\) for the q-integer of \(j\), and write \(w(n, k)\) for the (q, r)-Whitney number of the first kind \(w_{m,r,q}(n, k)\). Then for all natural numbers \(n\) and \(k\),

\[w(n + 1, k + 1) = q^{-n} \bigl( w(n, k) - (m [n]_q + r) \, w(n, k + 1) \bigr).\]
theorem whitneyFirst_succ_succ (m r q : ℂ) [NeZero q] (n k : ℕ) :
    whitneyFirst m r q (n + 1) (k + 1) =
      (q ^ n)⁻¹ *
        (whitneyFirst m r q n k -
          (m * qBrack q n + r) * whitneyFirst m r q n (k + 1))
Uses 2 · Used by 2

TheoremInitial value of the second-kind (q, r)-Whitney numbers#✓fully proved

For complex numbers \(m\), \(r\), \(q\), let \(W_{m,r,q}(i, j)\), for natural numbers \(i\) and \(j\), denote the \((q, r)\)-Whitney numbers of the second kind. Then \(W_{m,r,q}(0, 0) = 1\).

theorem whitneySecond_zero_zero (m r q : ℂ) : whitneySecond m r q 0 0 = 1
Uses 1 · Used by 2

TheoremRow zero of the second-kind (q, r)-Whitney numbers vanishes off the diagonal#✓fully proved

For complex numbers \(m\), \(r\), \(q\), let \(W_{m,r,q}(i, j)\), for natural numbers \(i\) and \(j\), denote the \((q, r)\)-Whitney numbers of the second kind. Then \(W_{m,r,q}(0, k + 1) = 0\) for every natural number \(k\).

theorem whitneySecond_zero_succ (m r q : ℂ) (k : ℕ) :
    whitneySecond m r q 0 (k + 1) = 0
Uses 1 · Used by 3

TheoremColumn-zero recurrence for second-kind (q, r)-Whitney numbers#✓fully proved

For complex numbers \(m\), \(r\), \(q\), let \(W_{m,r,q}(i, j)\), for natural numbers \(i\) and \(j\), denote the \((q, r)\)-Whitney numbers of the second kind. Then for every natural number \(n\), \(W_{m,r,q}(n + 1, 0) = r \, W_{m,r,q}(n, 0)\).

theorem whitneySecond_succ_zero (m r q : ℂ) (n : ℕ) :
    whitneySecond m r q (n + 1) 0 = r * whitneySecond m r q n 0
Uses 1 · Used by 2

TheoremTriangular recurrence for second-kind (q, r)-Whitney numbers#✓fully proved

For all complex numbers \(m\), \(r\), \(q\) and all natural numbers \(n\) and \(k\), the \((q, r)\)-Whitney numbers of the second kind \(W_{m,r,q}(n, k)\) satisfy

\[ W_{m,r,q}(n + 1, k + 1) = q^k \, W_{m,r,q}(n, k) + (m [k + 1]_q + r) \, W_{m,r,q}(n, k + 1), \]

where \([j]_q = 1 + q + \dots + q^{j-1}\) is the \(q\)-integer.

theorem whitneySecond_succ_succ (m r q : ℂ) (n k : ℕ) :
    whitneySecond m r q (n + 1) (k + 1) =
      q ^ k * whitneySecond m r q n k +
        (m * qBrack q (k + 1) + r) * whitneySecond m r q n (k + 1)
Uses 2 · Used by 4

TheoremFirst-kind (q, r)-Whitney numbers vanish above the diagonal#✓fully proved

For all complex numbers \(m, r, q\) with \(q \ne 0\) and all natural numbers \(n\) and \(k\) with \(n < k\), the (q, r)-Whitney number of the first kind satisfies \(w_{m,r,q}(n, k) = 0\).

theorem whitneyFirst_eq_zero_of_lt {m r q : ℂ} [NeZero q] {n k : ℕ} (h : n < k) :
    whitneyFirst m r q n k = 0
Uses 4

TheoremSecond-kind (q, r)-Whitney numbers vanish above the diagonal#✓fully proved

For all complex numbers \(m, r, q\) and all natural numbers \(n\) and \(k\) with \(n < k\), the (q, r)-Whitney number of the second kind satisfies \(W_{m,r,q}(n, k) = 0\).

theorem whitneySecond_eq_zero_of_lt {m r q : ℂ} {n k : ℕ} (h : n < k) :
    whitneySecond m r q n k = 0
Uses 4

TheoremTriangular recurrence for first-kind (q, r)-Whitney numbers, positive column form#✓fully proved

Let \(m, r, q\) be complex numbers with \(q \ne 0\), write \([j]_q\) for the q-integer of \(j\), and write \(w(n, k)\) for the (q, r)-Whitney number of the first kind \(w_{m,r,q}(n, k)\). Then for all natural numbers \(n\) and \(k\) with \(k \ge 1\),

\[w(n + 1, k) = q^{-n} \bigl( w(n, k - 1) - (m [n]_q + r) \, w(n, k) \bigr).\]
theorem whitneyFirst_succ_eq (m r q : ℂ) [NeZero q] (n k : ℕ) (hk : 1 ≤ k) :
    whitneyFirst m r q (n + 1) k =
      (q ^ n)⁻¹ *
        (whitneyFirst m r q n (k - 1) -
          (m * qBrack q n + r) * whitneyFirst m r q n k)
Uses 3

TheoremTriangular recurrence for second-kind (q, r)-Whitney numbers, positive column form#✓fully proved

Let \(m, r, q\) be complex numbers, write \([j]_q\) for the q-integer of \(j\), and write \(W(n, k)\) for the (q, r)-Whitney number of the second kind \(W_{m,r,q}(n, k)\). Then for all natural numbers \(n\) and \(k\) with \(k \ge 1\),

\[W(n + 1, k) = q^{k - 1} \, W(n, k - 1) + (m [k]_q + r) \, W(n, k).\]
theorem whitneySecond_succ_eq (m r q : ℂ) (n k : ℕ) (hk : 1 ≤ k) :
    whitneySecond m r q (n + 1) k =
      q ^ (k - 1) * whitneySecond m r q n (k - 1) +
        (m * qBrack q k + r) * whitneySecond m r q n k
Uses 3

Definition\((q, r)\)-Dowling polynomial#✓fully proved

Let \(R\) be a semiring and let \(W(n, k) \in R\) for all natural numbers \(n\) and \(k\) (intended to be the \((q, r)\)-Whitney numbers of the second kind, but any family is allowed). For a natural number \(n\), the \((q, r)\)-Dowling polynomial of \(W\) at \(n\) is the polynomial \(\sum_{k=0}^{n} W(n, k)\, x^k\) in \(R[x]\).

noncomputable def qrDowlingPolynomial (W : ℕ → ℕ → R) (n : ℕ) : Polynomial R :=
  ∑ k ∈ Finset.range (n + 1), Polynomial.C (W n k) * Polynomial.X ^ k
Used by 4

Definition\((q, r)\)-Dowling number#✓fully proved

Let \(R\) be a semiring and let \(W(n, k) \in R\) for all natural numbers \(n\) and \(k\). For a natural number \(n\), the \((q, r)\)-Dowling number of \(W\) at \(n\) is the value at \(x = 1\) of the \((q, r)\)-Dowling polynomial \(\sum_{k=0}^{n} W(n, k)\, x^k\) of \(W\).

noncomputable def qrDowlingNumber (W : ℕ → ℕ → R) (n : ℕ) : R :=
  Polynomial.eval 1 (qrDowlingPolynomial W n)
Uses 1 · Used by 4

Theorem\((q, r)\)-Dowling numbers as sums of coefficients#✓fully proved

Let \(R\) be a semiring and let \(W(n, k) \in R\) for all natural numbers \(n\) and \(k\). For every natural number \(n\), the \((q, r)\)-Dowling number of \(W\) at \(n\) equals \(\sum_{k=0}^{n} W(n, k)\).

theorem qrDowlingNumber_eq_sum (W : ℕ → ℕ → R) (n : ℕ) :
    qrDowlingNumber W n = ∑ k ∈ Finset.range (n + 1), W n k
Uses 2

Theorem(q, r)-Whitney numbers of the second kind through q-Stirling numbers#✓fully proved

Let \(m, r, q \in \mathbb{C}\) and write \([k + 1]_q = 1 + q + \dots + q^k\). Let \(S\) be a complex-valued function on pairs of natural numbers satisfying the recurrence of the \(q\)-Stirling numbers of the second kind: for all \(a, k \in \mathbb{N}\), \(S(0, 0) = 1\), \(S(0, k + 1) = 0\), \(S(a + 1, 0) = 0\) and \(S(a + 1, k + 1) = q^k S(a, k) + [k + 1]_q \, S(a, k + 1)\). Then for all \(a, k \in \mathbb{N}\) the \((q, r)\)-Whitney numbers of the second kind satisfy

\[W_{m,r,q}(a, k) = \sum_{j=0}^{a} \binom{a}{j} r^{a-j} m^{j-k} S(j, k),\]

where the exponent \(j - k\) is read as \(0\) when \(j < k\).

theorem QRWhitney.whitneySecond_eq_sum_qStirlingSecond
    (m r q : ℂ)
    (qStirlingSecond : ℕ → ℕ → ℂ)
    (hq_zero_zero : qStirlingSecond 0 0 = 1)
    (hq_zero_succ : ∀ k : ℕ, qStirlingSecond 0 (k + 1) = 0)
    (hq_succ_zero : ∀ a : ℕ, qStirlingSecond (a + 1) 0 = 0)
    (hq_succ_succ : ∀ a k : ℕ,
      qStirlingSecond (a + 1) (k + 1) =
        q ^ k * qStirlingSecond a k + QRWhitney.qBrack q (k + 1) * qStirlingSecond a (k + 1)) :
    ∀ a k : ℕ, QRWhitney.whitneySecond m r q a k =
      ∑ j ∈ Finset.range (a + 1),
        (Nat.choose a j : ℂ) * r ^ (a - j) * m ^ (j - k) *
          qStirlingSecond j k
Uses 6 · Used by 1

TheoremExpansion of the (q, r)-Dowling polynomial in q-Stirling numbers#✓fully proved

Let \(m, r, q, x \in \mathbb{C}\) and \(n \in \mathbb{N}\), and write \([k + 1]_q = 1 + q + \dots + q^k\). Let \(S\) be a complex-valued function on pairs of natural numbers satisfying the recurrence of the \(q\)-Stirling numbers of the second kind: for all \(a, k \in \mathbb{N}\), \(S(0, 0) = 1\), \(S(0, k + 1) = 0\), \(S(a + 1, 0) = 0\) and \(S(a + 1, k + 1) = q^k S(a, k) + [k + 1]_q \, S(a, k + 1)\). Let \(W_{m,r,q}\) be the \((q, r)\)-Whitney numbers of the second kind, and let \(D_n(x)\) be the value at \(x\) of the \((q, r)\)-Dowling polynomial \(\sum_{k=0}^{n} W_{m,r,q}(n, k) \, X^k\). Then

\[D_n(x) = \sum_{k=0}^{n} \binom{n}{k} r^{n-k} \sum_{j=0}^{k} m^{k-j} S(k, j) \, x^j.\]
theorem eval_qrDowlingPolynomial_whitneySecond
    (m r q x : ℂ) (n : ℕ)
    (qStirlingSecond : ℕ → ℕ → ℂ)
    (hq_zero_zero : qStirlingSecond 0 0 = 1)
    (hq_zero_succ : ∀ k : ℕ, qStirlingSecond 0 (k + 1) = 0)
    (hq_succ_zero : ∀ a : ℕ, qStirlingSecond (a + 1) 0 = 0)
    (hq_succ_succ : ∀ a k : ℕ,
      qStirlingSecond (a + 1) (k + 1) =
        q ^ k * qStirlingSecond a k + QRWhitney.qBrack q (k + 1) * qStirlingSecond a (k + 1)) :
    Polynomial.eval x (qrDowlingPolynomial (QRWhitney.whitneySecond m r q) n) =
      ∑ k ∈ Finset.range (n + 1),
        (Nat.choose n k : ℂ) * r ^ (n - k) *
          ∑ j ∈ Finset.range (k + 1),
            m ^ (k - j) * qStirlingSecond k j * x ^ j
Sources
Uses 4 · Used by 1

Theorem(q, r)-Dowling polynomial expansion from the defining recurrences#✓fully proved

Let \(q, m, r, x \in \mathbb{C}\) and \(n \in \mathbb{N}\), and write \([k + 1]_q = \sum_{i=0}^{k} q^i\). Let \(S\) and \(W\) be complex-valued functions on pairs of natural numbers, and let \(D(a, y)\) be a complex-valued function of \(a \in \mathbb{N}\) and \(y \in \mathbb{C}\), such that for all \(a, k \in \mathbb{N}\) and \(y \in \mathbb{C}\): \(S(0, 0) = 1\), \(S(0, k + 1) = 0\), \(S(a + 1, 0) = 0\) and \(S(a + 1, k + 1) = q^k S(a, k) + [k + 1]_q \, S(a, k + 1)\) (the recurrence of the \(q\)-Stirling numbers of the second kind); \(W(0, 0) = 1\), \(W(0, k + 1) = 0\), \(W(a + 1, 0) = r^{a + 1}\) and \(W(a + 1, k + 1) = q^k W(a, k) + (m [k + 1]_q + r) \, W(a, k + 1)\) (the recurrence of the \((q, r)\)-Whitney numbers of the second kind); and \(D(a, y) = \sum_{k=0}^{a} W(a, k) \, y^k\) (the \((q, r)\)-Dowling polynomial). Then

\[D(n, x) = \sum_{k=0}^{n} \binom{n}{k} r^{n-k} \sum_{j=0}^{k} m^{k-j} S(k, j) \, x^j.\]
MetaMathlibExt.q_r_dowling_polynomial_q_stirling_expansion · 27 lines
theorem q_r_dowling_polynomial_q_stirling_expansion
    (q m r x : ℂ) (n : ℕ)
    (qStirlingSecond whitneySecond : ℕ → ℕ → ℂ)
    (dowlingPolynomial : ℕ → ℂ → ℂ)
    (hq_zero_zero : qStirlingSecond 0 0 = 1)
    (hq_zero_succ : ∀ k : ℕ, qStirlingSecond 0 (k + 1) = 0)
    (hq_succ_zero : ∀ a : ℕ, qStirlingSecond (a + 1) 0 = 0)
    (hq_succ_succ : ∀ a k : ℕ,
      qStirlingSecond (a + 1) (k + 1) =
        q ^ k * qStirlingSecond a k +
          (∑ i ∈ Finset.range (k + 1), q ^ i) * qStirlingSecond a (k + 1))
    (hW_zero_zero : whitneySecond 0 0 = 1)
    (hW_zero_succ : ∀ k : ℕ, whitneySecond 0 (k + 1) = 0)
    (hW_succ_zero : ∀ a : ℕ, whitneySecond (a + 1) 0 = r ^ (a + 1))
    (hW_succ_succ : ∀ a k : ℕ,
      whitneySecond (a + 1) (k + 1) =
        q ^ k * whitneySecond a k +
          (m * (∑ i ∈ Finset.range (k + 1), q ^ i) + r) *
            whitneySecond a (k + 1))
    (hD : ∀ a : ℕ, ∀ y : ℂ,
      dowlingPolynomial a y =
        ∑ k ∈ Finset.range (a + 1), whitneySecond a k * y ^ k) :
    dowlingPolynomial n x =
      ∑ k ∈ Finset.range (n + 1),
        (Nat.choose n k : ℂ) * r ^ (n - k) *
          ∑ j ∈ Finset.range (k + 1),
            m ^ (k - j) * qStirlingSecond k j * x ^ j
Sources
Uses 8
21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.