Totienomial coefficients

DefinitionGeneralized factorial#✓fully proved

For a sequence \(f \colon \mathbb{N} \to \mathbb{N}\) and a natural number \(n\), the generalized factorial of \(f\) at \(n\) is the product \(f(1) f(2) \cdots f(n)\) of the values \(f(i)\) for \(1 \le i \le n\); for \(n = 0\) it is the empty product \(1\).

def generalizedFactorial (f : ℕ → ℕ) (n : ℕ) : ℕ :=
  Finset.prod (Finset.Icc 1 n) f
Sources
  • https://cs.uwaterloo.ca/journals/JIS/VOL19/Edgar/edgar3.tex
Used by 3
Used byGeneralized binomial coefficient · Defining equation of the generalized binomial coefficient · Generalized factorials of positive sequences are positive

DefinitionPositive sequence#✓fully proved

A sequence \(f \colon \mathbb{N} \to \mathbb{N}\) is positive when \(f(i) > 0\) for every \(i > 0\); the value \(f(0)\) is unrestricted.

This is the condition on \(f\) under which the source defines generalized binomial coefficients.

def IsPositiveSequence (f : ℕ → ℕ) : Prop :=
  ∀ i, 0 < i → 0 < f i
Used by 2
Used byDefining equation of the generalized binomial coefficient · Generalized factorials of positive sequences are positive

TheoremGeneralized factorials of positive sequences are positive#✓fully proved

Let \(f \colon \mathbb{N} \to \mathbb{N}\) be a positive sequence, that is \(f(i) > 0\) for every \(i > 0\). Then for every natural number \(n\), the generalized factorial \(f(1) f(2) \cdots f(n)\) is positive.

theorem generalizedFactorial_pos {f : ℕ → ℕ} (hf : IsPositiveSequence f) (n : ℕ) :
    0 < generalizedFactorial f n
Uses 2 · Used by 1
Statement usesPositive sequence · Generalized factorial
Used byDefining equation of the generalized binomial coefficient

DefinitionGeneralized binomial coefficient#✓fully proved

Let \(f \colon \mathbb{N} \to \mathbb{N}\) be a sequence and write \(k!_f = f(1) f(2) \cdots f(k)\) for its generalized factorial, so that \(0!_f = 1\). For natural numbers \(n\) and \(m\), the generalized binomial coefficient of \(f\) is the rational number

\[\binom{n+m}{n}_f = \frac{(n+m)!_f}{n!_f \, m!_f},\]

which is taken to be \(0\) when the denominator is \(0\).

When \(f(i) > 0\) for every \(i > 0\), the setting of the source, the denominator is never \(0\) and this is the source's quotient.

def generalizedBinomialCoefficient (f : ℕ → ℕ) (n m : ℕ) : ℚ :=
  (generalizedFactorial f (n + m) : ℚ) /
    ((generalizedFactorial f n : ℚ) * (generalizedFactorial f m : ℚ))
Sources
  • https://cs.uwaterloo.ca/journals/JIS/VOL19/Edgar/edgar3.tex
Uses 1 · Used by 4
Statement usesGeneralized factorial
Used byDefining equation of the generalized binomial coefficient · Totienomial coefficient · Lex-minimal extensions have a nomid coefficient equal to one · Nomid coefficients of binomid indices that are not lex-minimal extensions

TheoremDefining equation of the generalized binomial coefficient#✓fully proved

Let \(f \colon \mathbb{N} \to \mathbb{N}\) be a positive sequence, that is \(f(i) > 0\) for every \(i > 0\), and write \(k!_f = f(1) f(2) \cdots f(k)\) for its generalized factorial. Then for all natural numbers \(n\) and \(m\), the generalized binomial coefficient \(\binom{n+m}{n}_f\), defined as \((n+m)!_f / (n!_f \, m!_f)\) with division by \(0\) giving \(0\), satisfies \(\binom{n+m}{n}_f \cdot n!_f \, m!_f = (n+m)!_f\) in \(\mathbb{Q}\).

theorem generalizedBinomialCoefficient_mul_denominator {f : ℕ → ℕ}
    (hf : IsPositiveSequence f) (n m : ℕ) :
    generalizedBinomialCoefficient f n m *
        ((generalizedFactorial f n : ℚ) * (generalizedFactorial f m : ℚ)) =
      generalizedFactorial f (n + m)
Uses 4
Statement usesPositive sequence · Generalized binomial coefficient · Generalized factorial
Proof usesGeneralized factorials of positive sequences are positive

DefinitionTotienomial coefficient#✓fully proved

Let \(\varphi\) be Euler's totient function and write \(k!_\varphi = \varphi(1) \varphi(2) \cdots \varphi(k)\). For natural numbers \(n\) and \(m\), the totienomial coefficient is the generalized binomial coefficient of \(\varphi\), that is the rational number

\[\binom{n+m}{n}_\varphi = \frac{(n+m)!_\varphi}{n!_\varphi \, m!_\varphi}.\]

Since \(\varphi(i) > 0\) for every \(i > 0\), the denominator is never \(0\).

def totienomialCoefficient (n m : ℕ) : ℚ :=
  generalizedBinomialCoefficient Nat.totient n m
Sources
  • https://cs.uwaterloo.ca/journals/JIS/VOL19/Edgar/edgar3.tex
Uses 1 · Used by 1
Statement usesGeneralized binomial coefficient
Used byIntegrality and prime factorization of totienomial coefficients

TheoremIntegrality and prime factorization of totienomial coefficients#✓fully proved

For all natural numbers \(n\) and \(m\), the totienomial coefficient \(\binom{n+m}{n}_\varphi\) of Euler's totient function \(\varphi\) is a natural number, namely

\[\binom{n+m}{n}_\varphi = \prod_{p \le n+m} (p-1)^{c_p} \, p^{v_p(\binom{n+m}{n}) - c_p},\]

where the product runs over the primes \(p \le n+m\), \(\binom{n+m}{n}\) is the ordinary binomial coefficient, \(v_p\) is the \(p\)-adic valuation and \(c_p = \lfloor (n+m)/p \rfloor - \lfloor n/p \rfloor - \lfloor m/p \rfloor\).

Both exponents are natural numbers, since \(\lfloor n/p \rfloor + \lfloor m/p \rfloor \le \lfloor (n+m)/p \rfloor\) and \(c_p \le v_p(\binom{n+m}{n})\).

theorem totienomial_integral_factorization (n m : ℕ) :
    ∃ N : ℕ,
      totienomialCoefficient n m = (N : ℚ) ∧
      N = ∏ p ∈ Nat.primesLE (n + m),
        ((p - 1) ^ ((n + m) / p - n / p - m / p) *
          p ^ (Nat.factorization (Nat.choose (n + m) n) p -
            ((n + m) / p - n / p - m / p)))
Sources
Uses 1
Statement usesTotienomial coefficient
7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.