Pascal matrix

DefinitionEntries of the infinite Pascal matrix#✓fully proved

For natural numbers \(i\) and \(j\), the entry of the infinite Pascal matrix in row \(i\) and column \(j\) is the binomial coefficient \(\binom{i}{j}\).

public def pascalEntry (i j : ℕ) : ℕ :=
  Nat.choose i j

Used by 6

Used byColumn generating functions of the Pascal matrix · Closed form of the Pascal column generating functions · Summing the Pascal column generating functions · Total generating function of the Pascal matrix · Reversing the order of summation in the Pascal matrix · Summing the Pascal matrix row by row

DefinitionColumn generating functions of the Pascal matrix#✓fully proved

For a natural number \(j\) and a real number \(x\), the column generating function of the infinite Pascal matrix is \(\alpha_j(x) = \sum_{i \ge 0} \binom{i}{j} x^i\), where \(\binom{i}{j}\) is the entry in row \(i\) and column \(j\); the sum is taken to be \(0\) when the series is not summable.

public noncomputable def pascalAlpha (j : ℕ) (x : ℝ) : ℝ :=
  ∑' i, (pascalEntry i j : ℝ) * x ^ i

Uses 1 · Used by 3

Statement usesEntries of the infinite Pascal matrix

Used byClosed form of the Pascal column generating functions · Summing the Pascal column generating functions · Total generating function of the Pascal matrix

TheoremClosed form of the Pascal column generating functions#✓fully proved

For every natural number \(j\) and every real number \(x\) with \(|x| < 1\), the column generating function \(\alpha_j\) of the infinite Pascal matrix satisfies \(\alpha_j(x) = x^j / (1 - x)^{j+1}\).

public theorem pascalAlpha_eq (j : ℕ) (x : ℝ) (hx : |x| < 1) :
    pascalAlpha j x = x ^ j / (1 - x) ^ (j + 1)

Uses 2 · Used by 1

Statement usesColumn generating functions of the Pascal matrix

Proof usesEntries of the infinite Pascal matrix

Used bySumming the Pascal column generating functions

TheoremSumming the Pascal column generating functions#✓fully proved

For every real number \(x\) with \(|x| < 1/2\), the sum \(\sum_{j \ge 0} \alpha_j(x)\) of the column generating functions of the infinite Pascal matrix equals \(\sum_{j \ge 0} \sum_{i \ge 0} \binom{i}{j} x^i\), where \(\binom{i}{j}\) is the entry in row \(i\) and column \(j\), and it also equals \(\sum_{j \ge 0} x^j / (1 - x)^{j+1}\).

public theorem tsum_pascalAlpha_eq (x : ℝ) (hx : |x| < 1 / 2) :
    (∑' j, pascalAlpha j x) = (∑' j, ∑' i, (pascalEntry i j : ℝ) * x ^ i) ∧
      (∑' j, pascalAlpha j x) = ∑' j, x ^ j / (1 - x) ^ (j + 1)

Uses 3 · Used by 1

Statement usesColumn generating functions of the Pascal matrix · Entries of the infinite Pascal matrix

Proof usesClosed form of the Pascal column generating functions

Used byTotal generating function of the Pascal matrix

TheoremReversing the order of summation in the Pascal matrix#✓fully proved

For every real number \(x\) with \(|x| < 1/2\), writing \(\binom{i}{j}\) for the entry of the infinite Pascal matrix in row \(i\) and column \(j\), we have \(\sum_{j \ge 0} \sum_{i \ge 0} \binom{i}{j} x^i = \sum_{i \ge 0} \sum_{j \ge 0} \binom{i}{j} x^i\), and this sum equals \(\frac{1}{1 - x} \sum_{j \ge 0} \left(\frac{x}{1 - x}\right)^j\).

public theorem tsum_pascalEntry_comm (x : ℝ) (hx : |x| < 1 / 2) :
    (∑' j, ∑' i, (pascalEntry i j : ℝ) * x ^ i) =
      (∑' i, ∑' j, (pascalEntry i j : ℝ) * x ^ i) ∧
    (∑' i, ∑' j, (pascalEntry i j : ℝ) * x ^ i) =
      (1 / (1 - x)) * (∑' j, (x / (1 - x)) ^ j)

Uses 1 · Used by 1

Statement usesEntries of the infinite Pascal matrix

Used byTotal generating function of the Pascal matrix

TheoremSumming the Pascal matrix row by row#✓fully proved

For every real number \(x\) with \(|x| < 1/2\), writing \(\binom{i}{j}\) for the entry of the infinite Pascal matrix in row \(i\) and column \(j\), we have \(\sum_{i \ge 0} x^i \sum_{j=0}^{i} \binom{i}{j} = \frac{1}{1 - 2x}\).

public theorem tsum_pascalEntry_row (x : ℝ) (hx : |x| < 1 / 2) :
    (∑' i, x ^ i * Finset.sum (Finset.range (i + 1))
      (fun j => (pascalEntry i j : ℝ))) = 1 / (1 - 2 * x)

Uses 1

Statement usesEntries of the infinite Pascal matrix

TheoremTotal generating function of the Pascal matrix#✓fully proved

For every real number \(x\) with \(|x| < 1/2\), the sum \(\sum_{j \ge 0} \alpha_j(x)\) of the column generating functions of the infinite Pascal matrix equals \(\sum_{i \ge 0} (2x)^i\), and \(\sum_{i \ge 0} (2x)^i = \frac{1}{1 - 2x}\).

public theorem tsum_pascalAlpha_eq_geometric (x : ℝ) (hx : |x| < 1 / 2) :
    (∑' j, pascalAlpha j x) = (∑' i, (2 * x) ^ i) ∧
      (∑' i, (2 * x) ^ i) = 1 / (1 - 2 * x)

Uses 4

Statement usesColumn generating functions of the Pascal matrix

Proof usesEntries of the infinite Pascal matrix · Summing the Pascal column generating functions · Reversing the order of summation in the Pascal matrix

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.