Motzkin triangle

11 fully proved

Motzkin discriminant and Riordan pairs

DefinitionMotzkin discriminant#✓fully proved

The Motzkin discriminant is the formal power series \(1 - 2X - 3X^2 \in \mathbb{Q}[[X]]\), the discriminant in the generating functions for the Motzkin triangle.

noncomputable def motzkinDiscriminant : PowerSeries ℚ :=
  PowerSeries.C 1 - PowerSeries.C 2 * PowerSeries.X -
    PowerSeries.C 3 * PowerSeries.X ^ 2

Used by 4

Used bySquare roots of the Motzkin discriminant · The canonical Motzkin Riordan pair · Canonical square root of the Motzkin discriminant · Initial rows of the Motzkin triangle

DefinitionSquare roots of the Motzkin discriminant#✓fully proved

A formal power series \(s \in \mathbb{Q}[[X]]\) is a Motzkin square root when \(s^2 = 1 - 2X - 3X^2\) and the constant coefficient of \(s\) is \(1\).

def IsMotzkinSquareRoot (s : PowerSeries ℚ) : Prop :=
  s * s = motzkinDiscriminant ∧ PowerSeries.constantCoeff s = 1

Uses 1 · Used by 3

Statement usesMotzkin discriminant

Used byMotzkin Riordan pairs · The canonical Motzkin Riordan pair · Initial rows of the Motzkin triangle

DefinitionCanonical square root of the Motzkin discriminant#✓fully proved

The canonical square root is the power series \(s = \sum_{n \ge 0} \binom{1/2}{n} (-2X - 3X^2)^n \in \mathbb{Q}[[X]]\), obtained by substituting \(-2X - 3X^2\) for \(Y\) in the binomial series \((1 + Y)^{1/2} = \sum_{n \ge 0} \binom{1/2}{n} Y^n\).

It is the branch of \(\sqrt{1 - 2X - 3X^2}\) with constant coefficient \(1\) used by the Motzkin generating functions.

noncomputable def motzkinSquareRoot : PowerSeries ℚ :=
  (PowerSeries.binomialSeries ℚ (1 / 2 : ℚ)).subst (motzkinDiscriminant - 1)

Uses 1 · Used by 4

Statement usesMotzkin discriminant

Used byFirst component of the Motzkin Riordan pair · Second component of the Motzkin Riordan pair · The canonical Motzkin Riordan pair · Initial rows of the Motzkin triangle

DefinitionSecond component of the Motzkin Riordan pair#✓fully proved

Let \(s = \sum_{n \ge 0} \binom{1/2}{n} (-2X - 3X^2)^n \in \mathbb{Q}[[X]]\) be the canonical square root of \(1 - 2X - 3X^2\). The power series \(h \in \mathbb{Q}[[X]]\) has \(n\)-th coefficient \(\frac{1}{2} [X^{n+1}] (1 - X - s)\) for every \(n \ge 0\). Since \(1 - X - s\) has constant coefficient \(0\), this is the quotient \(h = (1 - X - s)/(2X)\).

The definition uses a coefficient shift so that no division by \(X\) is required.

noncomputable def motzkinH : PowerSeries ℚ :=
  PowerSeries.mk fun n ↦
    PowerSeries.coeff (n + 1) (1 - PowerSeries.X - motzkinSquareRoot) / 2

Uses 1 · Used by 2

Statement usesCanonical square root of the Motzkin discriminant

Used byThe canonical Motzkin Riordan pair · Initial rows of the Motzkin triangle

DefinitionFirst component of the Motzkin Riordan pair#✓fully proved

Let \(s = \sum_{n \ge 0} \binom{1/2}{n} (-2X - 3X^2)^n \in \mathbb{Q}[[X]]\) be the canonical square root of \(1 - 2X - 3X^2\), which has constant coefficient \(1\). The power series \(g \in \mathbb{Q}[[X]]\) is the multiplicative inverse \(g = s^{-1}\) of \(s\), that is, \(g = 1/\sqrt{1 - 2X - 3X^2}\).

noncomputable def motzkinG : PowerSeries ℚ :=
  motzkinSquareRoot⁻¹

Uses 1 · Used by 2

Statement usesCanonical square root of the Motzkin discriminant

Used byThe canonical Motzkin Riordan pair · Initial rows of the Motzkin triangle

DefinitionMotzkin Riordan pairs#✓fully proved

Formal power series \(g, h \in \mathbb{Q}[[X]]\) form a Motzkin Riordan pair when there is a power series \(s \in \mathbb{Q}[[X]]\) with \(s^2 = 1 - 2X - 3X^2\) and constant coefficient \(1\) such that \(g s = 1\) and \(2 X h = 1 - X - s\).

Writing the second identity without division by \(X\) keeps the characterization internal to formal power series. The constant-coefficient condition selects the intended square-root branch.

def IsMotzkinRiordanPair (g h : PowerSeries ℚ) : Prop :=
  ∃ s : PowerSeries ℚ,
    IsMotzkinSquareRoot s ∧ g * s = 1 ∧
      2 * PowerSeries.X * h = 1 - PowerSeries.X - s

Uses 1 · Used by 2

Statement usesSquare roots of the Motzkin discriminant

Used byBundled Motzkin Riordan pairs · The canonical Motzkin Riordan pair

StructureBundled Motzkin Riordan pairs#✓fully proved

A bundled Motzkin Riordan pair consists of formal power series \(g, h \in \mathbb{Q}[[X]]\) together with a proof that they form a Motzkin Riordan pair: there is \(s \in \mathbb{Q}[[X]]\) with \(s^2 = 1 - 2X - 3X^2\) and constant coefficient \(1\) such that \(g s = 1\) and \(2 X h = 1 - X - s\).

structure MotzkinRiordanPair where
  g : PowerSeries ℚ
  h : PowerSeries ℚ
  isPair : IsMotzkinRiordanPair g h

Uses 1 · Used by 3

Statement usesMotzkin Riordan pairs

Used byEntries of a Motzkin Riordan array · The canonical Motzkin Riordan pair · Initial rows of the Motzkin triangle

Motzkin Riordan Pair

DefinitionEntries of a Motzkin Riordan array#✓fully proved

For a Motzkin Riordan pair \((g, h)\) and natural numbers \(n\) and \(k\), the \((n, k)\) entry is the rational number \([X^n]\, g h^k\), the coefficient of \(X^n\) in the power series \(g h^k \in \mathbb{Q}[[X]]\).

noncomputable def entry (p : MotzkinRiordanPair) (n k : ℕ) : ℚ :=
  PowerSeries.coeff n (p.g * p.h ^ k)

Uses 1 · Used by 1

Statement usesBundled Motzkin Riordan pairs

Used byMotzkin triangle

Motzkin triangle

DefinitionThe canonical Motzkin Riordan pair#✓fully proved

Let \(s \in \mathbb{Q}[[X]]\) be the canonical square root of \(1 - 2X - 3X^2\), given by the binomial series, which has constant coefficient \(1\). The canonical Motzkin Riordan pair is \((g, h)\) with \(g = s^{-1}\) and \(h = (1 - X - s)/(2X)\), the Motzkin Riordan pair conditions being witnessed by \(s\).

noncomputable def motzkinRiordanPair : MotzkinRiordanPair where
  g := motzkinG
  h := motzkinH
  isPair := ⟨motzkinSquareRoot, motzkinSquareRoot_isSquareRoot,
    motzkinG_mul_motzkinSquareRoot, two_mul_X_mul_motzkinH⟩

Uses 7 · Used by 2

Statement usesMotzkin Riordan pairs · Square roots of the Motzkin discriminant · Bundled Motzkin Riordan pairs · Motzkin discriminant · First component of the Motzkin Riordan pair · Second component of the Motzkin Riordan pair · Canonical square root of the Motzkin discriminant

Used byMotzkin triangle · Initial rows of the Motzkin triangle

DefinitionMotzkin triangle#✓fully proved

Let \(s\) be the square root of \(1 - 2X - 3X^2\) in the ring of formal power series over \(\mathbb{Q}\) with constant coefficient \(1\), and let \(g = 1/s\) and \(h = (1 - X - s)/(2X)\). For natural numbers \(n\) and \(k\), the \((n, k)\) entry of the Motzkin triangle (OEIS A094531) is the rational number given by the coefficient of \(X^n\) in \(g h^k\).

noncomputable def motzkinTriangle (n k : ℕ) : ℚ :=
  motzkinRiordanPair.entry n k

Uses 2 · Used by 1

Statement usesEntries of a Motzkin Riordan array · The canonical Motzkin Riordan pair

Used byInitial rows of the Motzkin triangle

TheoremInitial rows of the Motzkin triangle#✓fully proved

Writing \(T(n, k)\) for the \((n, k)\) entry of the canonical Motzkin triangle, the rows \(n = 0, 1, 2, 3\) (with \(0 \le k \le n\)) are \(T(0, 0) = 1\); \(T(1, 0) = T(1, 1) = 1\); \(T(2, 0) = 3\), \(T(2, 1) = 2\), \(T(2, 2) = 1\); and \(T(3, 0) = 7\), \(T(3, 1) = 6\), \(T(3, 2) = 3\), \(T(3, 3) = 1\), matching OEIS A094531.

theorem motzkinTriangle_initial_rows :
    [[motzkinTriangle 0 0],
      [motzkinTriangle 1 0, motzkinTriangle 1 1],
      [motzkinTriangle 2 0, motzkinTriangle 2 1, motzkinTriangle 2 2],
      [motzkinTriangle 3 0, motzkinTriangle 3 1,
        motzkinTriangle 3 2, motzkinTriangle 3 3]] =
    [[1], [1, 1], [3, 2, 1], [7, 6, 3, 1]]

Uses 8

Statement usesMotzkin triangle

Proof usesSquare roots of the Motzkin discriminant · Bundled Motzkin Riordan pairs · Motzkin discriminant · First component of the Motzkin Riordan pair · Second component of the Motzkin Riordan pair · The canonical Motzkin Riordan pair · Canonical square root of the Motzkin discriminant

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.