Simsek numbers

DefinitionSimsek numbers#✓fully proved

For natural numbers \(n\) and \(k\) and a complex number \(\lambda\), the Simsek number \(y_1(n, k; \lambda)\) is the complex number

\[y_1(n, k; \lambda) = \frac{1}{k!} \sum_{j=0}^{k} \binom{k}{j} j^n \lambda^j,\]

where \(0^0 = 1\).

public noncomputable def simsekNumber (n k : Nat) (lam : ℂ) : ℂ :=
  ((k.factorial : ℂ))⁻¹ *
    ∑ j ∈ Finset.range (k + 1), (k.choose j : ℂ) * (((j : ℂ) ^ n) * (lam ^ j))

Sources

• equation (snmf1) of https://cs.uwaterloo.ca/journals/JIS/VOL26/Oussi/oussi9.tex.

Used by 3

Used byFinite-sum formula for Simsek numbers · Simsek numbers with second index zero · Simsek numbers with both indices zero

TheoremFinite-sum formula for Simsek numbers#✓fully proved

For all natural numbers \(n\) and \(k\) and every complex number \(\lambda\), the Simsek number satisfies \(y_1(n, k; \lambda) = \frac{1}{k!} \sum_{j=0}^{k} \binom{k}{j} j^n \lambda^j\), where \(0^0 = 1\).

public theorem simsekNumber_eq_sum (n k : Nat) (lam : ℂ) :
    simsekNumber n k lam =
      ((k.factorial : ℂ))⁻¹ *
        ∑ j ∈ Finset.range (k + 1), (k.choose j : ℂ) * (((j : ℂ) ^ n) * (lam ^ j))

Uses 1

Statement usesSimsek numbers

TheoremSimsek numbers with second index zero#✓fully proved

For every natural number \(n\) and every complex number \(\lambda\), the Simsek number \(y_1(n, 0; \lambda)\) equals \(0^n\); that is, it equals \(1\) when \(n = 0\) and \(0\) otherwise.

public theorem simsekNumber_zero_k (n : Nat) (lam : ℂ) :
    simsekNumber n 0 lam = (0 : ℂ) ^ n

Uses 1

Statement usesSimsek numbers

TheoremSimsek numbers with both indices zero#✓fully proved

For every complex number \(\lambda\), the Simsek number \(y_1(0, 0; \lambda)\) equals \(1\).

public theorem simsekNumber_zero_zero (lam : ℂ) :
    simsekNumber 0 0 lam = 1

Uses 1

Statement usesSimsek numbers

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.