Orthogonal polynomials and polynomial sequences

Classical and combinatorial families of polynomials, their recurrences and generating functions, and orthogonality via Favard's theorem, J-fractions and Riordan arrays.

TheoremBinomial theorem for rising factorials#✓fully proved

For every natural number \(n\) and all real numbers \(a\) and \(b\), writing \(x^{\overline{m}} = x(x+1)\cdots(x+m-1)\) for the rising factorial,

\[(a+b)^{\overline{n}} = \sum_{k=0}^{n} \binom{n}{k}\, a^{\overline{k}}\, b^{\overline{n-k}}.\]
theorem ascPochhammer_eval_add (n : ℕ) (a b : ℝ) :
    (ascPochhammer ℝ n).eval (a + b) =
      ∑ k ∈ Finset.range (n + 1), (n.choose k : ℝ) *
        (ascPochhammer ℝ k).eval a *
        (ascPochhammer ℝ (n - k)).eval b
Sources
  • Paul Eloe and Catherine Kublik, "When Numerical Analysis Crosses Paths with Catalan and Generalized Motzkin Numbers," Journal of Integer Sequences 21 (2018), Article 18.8.4, Theorem, equation, lines 156–161, https://cs.uwaterloo.ca/journals/JIS/VOL21/Kublik/kublik2.tex
Used by 1
Used byBase-\(b\) generalized digital binomial theorem

StructureClassical orthogonal polynomial family#✓fully proved

A classical orthogonal polynomial family consists of real polynomials \(P_0, P_1, P_2, \dots\), each \(P_n\) monic of degree exactly \(n\), a measure \(\mu\) on \(\mathbb{R}\), a measurable set \(D \subseteq \mathbb{R}\) that is an interval with nonempty interior, and a function \(w : \mathbb{R} \to \mathbb{R}\) (the weight), such that \(w(x) \ge 0\) for every \(x \in D\); \(\mu\) is the measure with density \(w\) with respect to Lebesgue measure restricted to \(D\); \(\int P_m P_n \, d\mu = 0\) whenever \(m \ne n\); \(\int P_n^2 \, d\mu \ne 0\) for every \(n\); and there are real numbers \(u_0, u_1, v_0, v_1, v_2\), with \(v_0, v_1, v_2\) not all zero, such that at every interior point \(x\) of \(D\) the weight is differentiable and \((v_0 + v_1 x + v_2 x^2) \, w'(x) = (u_0 + u_1 x) \, w(x)\) (the Pearson equation).

MetaMathlibExt.ClassicalOrthogonalPolynomialFamily · 42 lines 
structure ClassicalOrthogonalPolynomialFamily where
  /-- Sequence of real polynomials (concept `jis_sem_6573fe45e3bbd4f163aed756`). -/
  P : ℕ → Polynomial ℝ
  /-- The source uses the monic normalization of the polynomial family. -/
  monic : ∀ n : ℕ, (P n).Monic
  /-- The `n`th member has degree exactly `n`. -/
  natDegree_eq : ∀ n : ℕ, (P n).natDegree = n
  /-- Orthogonalizing measure (concept `jis_sem_6573fe45e3bbd4f163aed756`). -/
  μ : MeasureTheory.Measure ℝ
  /-- Supporting domain for the weight density (source block `jis_srcblock_e90c95146a5fe658`). -/
  domain : Set ℝ
  /-- The domain is measurable (source block `jis_srcblock_e90c95146a5fe658`). -/
  measurable_domain : MeasurableSet domain
  /-- The support domain is an interval, as in the classical families. -/
  ordConnected_domain : Set.OrdConnected domain
  /-- The support interval has nonempty interior, so the Pearson equation is not vacuous. -/
  interior_domain_nonempty : (interior domain).Nonempty
  /-- Distinct members are orthogonal with respect to `μ`
      (concept `jis_sem_6573fe45e3bbd4f163aed756`). -/
  orthogonal : ∀ m n : ℕ, m ≠ n →
    MeasureTheory.integral μ (fun x => Polynomial.eval x (P m) * Polynomial.eval x (P n)) = 0
  /-- Each squared norm is nonzero, excluding the zero family
      (concept `jis_sem_6573fe45e3bbd4f163aed756`). -/
  norm_ne_zero : ∀ n : ℕ,
    MeasureTheory.integral μ (fun x => (Polynomial.eval x (P n)) ^ 2) ≠ 0
  /-- Nonnegative weight function (source block `jis_srcblock_e90c95146a5fe658`). -/
  weight : ℝ → ℝ
  /-- The weight is nonnegative (source block `jis_srcblock_e90c95146a5fe658`). -/
  weight_nonneg : ∀ x ∈ domain, 0 ≤ weight x
  /-- The measure is the weight density against restricted Lebesgue volume
      (source block `jis_srcblock_e90c95146a5fe658`). -/
  measure_eq : μ = (MeasureTheory.volume.restrict domain).withDensity
    (fun x => ENNReal.ofReal (weight x))
  /-- Classical Pearson equation `V w' = U w`, where `U` is linear and `V` is a genuinely
      nonzero quadratic polynomial. This cross-multiplied form remains meaningful at zeros of
      `V` or `w` (source block `jis_srcblock_e90c95146a5fe658`). -/
  classical : ∃ u0 u1 v0 v1 v2 : ℝ,
    (v0 ≠ 0 ∨ v1 ≠ 0 ∨ v2 ≠ 0) ∧
      ∀ x : ℝ, x ∈ interior domain →
        DifferentiableAt ℝ weight x ∧
          (v0 + v1 * x + v2 * x ^ 2) * deriv weight x =
            (u0 + u1 * x) * weight x

TheoremMeixner-type characterization of Riordan orthogonal polynomial arrays#✓fully proved

Let \(d\) and \(h\) be real formal power series with \([x^0]\,h = 0\), \([x^1]\,h \ne 0\) and \([x^0]\,d \ne 0\), where \([x^n]\) denotes the coefficient of \(x^n\), and let \(L\) be the Riordan array of \((d, h)\), with entries \(L_{n,k} = [x^n]\,(d h^k)\) for \(n, k \ge 0\). Call \(L\) a monic orthogonal coefficient array if there are real polynomials \(P_0, P_1, \dots\) with \([x^k]\,P_n = L_{n,k}\) for all \(n, k\), each \(P_n\) monic, and the family \((P_n)\) formally orthogonal. Each of the following three conditions is equivalent to \(L\) being a monic orthogonal coefficient array.

  1. Meixner form: there are real numbers \(\lambda, \mu, r, s\) with \(s \ne 0\) and \(s + \mu \ne 0\) such that \(d\,(1 + r x + s x^2) = 1 - \lambda x - \mu x^2\) and \(h\,(1 + r x + s x^2) = x\).
  2. Stieltjes form of the inverse: \(L_{0,0} = 1\), and there are an array \((L'_{n,k})\) and real numbers \(r_1, s_1, r, s\) with \(s_1 \ne 0\) and \(s \ne 0\) such that \(L_{n,k} = L'_{n,k} = 0\) whenever \(k > n\); \(\sum_{j=0}^{n} L_{n,j} L'_{j,k}\) and \(\sum_{j=0}^{n} L'_{n,j} L_{j,k}\) both equal \(1\) if \(n = k\) and \(0\) otherwise; and \(L'_{n+1,k} = \sum_{j=0}^{n+1} L'_{n,j} S_{j,k}\) for all \(n, k\), where \(S\) is the Stieltjes matrix with parameters \(r_1, s_1, r, s\): its superdiagonal entries are \(1\), its diagonal is \(r_1, r, r, \dots\), its subdiagonal is \(s_1, s, s, \dots\), and all other entries are \(0\).
  3. Coefficient recurrence: there are real numbers \(\lambda, \mu, r, s\) with \(s \ne 0\) and \(s + \mu \ne 0\) such that for all \(N, K \ge 0\), \(L_{N,K} + r L_{N-1,K} - L_{N-1,K-1} + s L_{N-2,K} = c_{N,K}\), where any entry of \(L\) with a negative index is read as \(0\), \(c_{0,0} = 1\), \(c_{1,0} = -\lambda\), \(c_{2,0} = -\mu\), and \(c_{N,K} = 0\) otherwise.

Proof: The coefficient recurrence is the common hub. The Meixner equivalence follows from Barry-Hennessy, the orthogonality equivalence from Favard's theorem as in Chihara, and the inverse-array equivalence from the Stieltjes production construction of the inverse array.

MetaMathlibExt.riordan_coeff_orth_equiv · 37 lines 
public theorem riordan_coeff_orth_equiv :
    ∀ (d h : PowerSeries ℝ) (L : ℕ → ℕ → ℝ),
      (PowerSeries.coeff 0 h = 0 ∧ PowerSeries.coeff 1 h ≠ 0 ∧
        PowerSeries.coeff 0 d ≠ 0 ∧
        ∀ n k : ℕ, L n k = PowerSeries.coeff n (d * h ^ k)) →
      let IsMonicOrthogonalCoeffArray :=
        ∃ P : ℕ → Polynomial ℝ,
          (∀ n k : ℕ, Polynomial.coeff (P n) k = L n k) ∧
          (∀ n : ℕ, (P n).Monic) ∧ Polynomial.IsFormallyOrthogonal P
      (IsMonicOrthogonalCoeffArray ↔
          ∃ lam mu r s : ℝ, s ≠ 0 ∧ s + mu ≠ 0 ∧
            d * (1 + PowerSeries.C r * (PowerSeries.X : PowerSeries ℝ) +
                PowerSeries.C s * (PowerSeries.X : PowerSeries ℝ) ^ 2) =
              1 - PowerSeries.C lam * (PowerSeries.X : PowerSeries ℝ) -
                PowerSeries.C mu * (PowerSeries.X : PowerSeries ℝ) ^ 2 ∧
            h * (1 + PowerSeries.C r * (PowerSeries.X : PowerSeries ℝ) +
                PowerSeries.C s * (PowerSeries.X : PowerSeries ℝ) ^ 2) =
              (PowerSeries.X : PowerSeries ℝ)) ∧
        (IsMonicOrthogonalCoeffArray ↔
          ∃ Linv : ℕ → ℕ → ℝ, ∃ r₁ s₁ r s : ℝ, L 0 0 = 1 ∧ s₁ ≠ 0 ∧ s ≠ 0 ∧
            (∀ n k : ℕ, k > n → L n k = 0) ∧
            (∀ n k : ℕ, k > n → Linv n k = 0) ∧
            (∀ n k : ℕ, (∑ j ∈ Finset.range (n + 1), L n j * Linv j k) =
              (if n = k then 1 else 0)) ∧
            (∀ n k : ℕ, (∑ j ∈ Finset.range (n + 1), Linv n j * L j k) =
              (if n = k then 1 else 0)) ∧
            (∀ n k : ℕ, Linv (n + 1) k =
              ∑ j ∈ Finset.range (n + 2), Linv n j * stieltjesMatrix r₁ s₁ r s j k)) ∧
        (IsMonicOrthogonalCoeffArray ↔
          ∃ lam mu r s : ℝ, s ≠ 0 ∧ s + mu ≠ 0 ∧
            ∀ N K : ℕ,
              L N K + r * (if 1 ≤ N then L (N - 1) K else 0) -
                  (if 1 ≤ N ∧ 1 ≤ K then L (N - 1) (K - 1) else 0) +
                  s * (if 2 ≤ N then L (N - 2) K else 0) =
                (if K = 0 then
                  if N = 0 then 1 else if N = 1 then -lam else if N = 2 then -mu else 0
                else 0))
Sources
  • Paul Barry and Aoife Hennessy, "Meixner-Type Results for Riordan Arrays and Associated Integer Sequences," Journal of Integer Sequences 13 (2010), Article 10.9.4, Proposition (referee's summary of the main results), lines 733–752, https://cs.uwaterloo.ca/journals/JIS/VOL13/Barry5/barry96s.tex
Uses 3
Statement usesFormally orthogonal polynomial family · Tridiagonal Stieltjes production matrix
Proof usesFavard's theorem
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.