Favard's theorem

DefinitionFormally orthogonal polynomial family#✓fully proved

Let \(R\) be a field. A family \((p_n)_{n \ge 0}\) of polynomials over \(R\) is formally orthogonal if there is an \(R\)-linear functional \(L \colon R[x] \to R\) such that each \(p_n\) has degree \(n\), \(L(p_n p_m) = 0\) whenever \(n \ne m\), and \(L(p_n^2) \ne 0\) for every \(n\).

public def IsFormallyOrthogonal {R : Type*} [Field R]
    (p : ℕ → Polynomial R) : Prop :=
  ∃ L : Polynomial R →ₗ[R] R, (∀ n, (p n).natDegree = n) ∧
    (∀ n m, n ≠ m → L (p n * p m) = 0) ∧ ∀ n, L (p n ^ 2) ≠ 0

Sources

• Barry, JIS VOL14 (Barry1/barry97r2.tex), lines 326-331. URL: https://cs.uwaterloo.ca/journals/JIS/VOL14/Barry1/barry97r2.tex

Used by 3

Used byFavard's theorem, forward direction · Favard's theorem · Meixner-type characterization of Riordan orthogonal polynomial arrays

TheoremFavard's theorem, forward direction#✓fully proved

Let \(R\) be a field and let \((p_n)_{n \ge 0}\) be a formally orthogonal family of monic polynomials over \(R\). Then there are sequences \((\alpha_n)_{n \ge 0}\) and \((\beta_n)_{n \ge 0}\) in \(R\) with \(\beta_n \ne 0\) for all \(n \ge 1\) such that \(p_0 = 1\), \(p_1 = x - \alpha_0\), and \(p_{n+1} = (x - \alpha_n) \, p_n - \beta_n \, p_{n-1}\) for all \(n \ge 1\).

public theorem favard_forward
    {R : Type*} [Field R] (p : ℕ → Polynomial R)
    (hmonic : ∀ n, (p n).Monic)
    (horth : Polynomial.IsFormallyOrthogonal p) :
    ∃ (α β : ℕ → R), (∀ n, β (n + 1) ≠ 0) ∧ p 0 = 1 ∧
      p 1 = Polynomial.X - Polynomial.C (α 0) ∧
      ∀ n, p (n + 2) = (Polynomial.X - Polynomial.C (α (n + 1))) *
        p (n + 1) - Polynomial.C (β (n + 1)) * p n

Sources

• Barry, JIS VOL14 (Barry1/barry97r2.tex), lines 346-352. URL: https://cs.uwaterloo.ca/journals/JIS/VOL14/Barry1/barry97r2.tex

Uses 1 · Used by 1

Statement usesFormally orthogonal polynomial family

Used byFavard's theorem

TheoremFavard's theorem#✓fully proved

Let \(R\) be a field and let \((p_n)_{n \ge 0}\) be a family of monic polynomials in \(R[x]\). Then \((p_n)\) is formally orthogonal if and only if there are sequences \((\alpha_n)_{n \ge 0}\) and \((\beta_n)_{n \ge 0}\) in \(R\) with \(\beta_n \ne 0\) for all \(n \ge 1\) such that \(p_0 = 1\), \(p_1 = x - \alpha_0\), and \(p_{n+1} = (x - \alpha_n) \, p_n - \beta_n \, p_{n-1}\) for all \(n \ge 1\).

theorem favard_iff
    {R : Type*} [Field R] (p : ℕ → Polynomial R)
    (hmonic : ∀ n, (p n).Monic) :
    Polynomial.IsFormallyOrthogonal p ↔
      ∃ (α β : ℕ → R), (∀ n, β (n + 1) ≠ 0) ∧ p 0 = 1 ∧
        p 1 = Polynomial.X - Polynomial.C (α 0) ∧
        ∀ n, p (n + 2) = (Polynomial.X - Polynomial.C (α (n + 1))) *
          p (n + 1) - Polynomial.C (β (n + 1)) * p n

Sources

• Paul Barry, "Riordan Arrays, Orthogonal Polynomials as Moments, and Hankel Transforms," Journal of Integer Sequences 14 (2011), Article 11.2.2, https://cs.uwaterloo.ca/journals/JIS/VOL14/Barry1/barry97r2.tex, Favard theorem at lines 346–352.

Uses 2 · Used by 1

Statement usesFormally orthogonal polynomial family

Proof usesFavard's theorem, forward direction

Used byMeixner-type characterization of Riordan orthogonal polynomial arrays

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.