LeanFun RevOLVER

3.3 Ultraspherical, Legendre and Chebyshev as Jacobi cases

The Jacobi family includes Gegenbauer, Legendre and both Chebyshev families after the normalizations described here. These identifications connect their formulas and weighted expansions.

3.3.1 Gegenbauer polynomials

The ultraspherical family is a rescaling of the symmetric Jacobi family. Its polynomial definition remains meaningful at degenerate parameters, including \(\lambda =0\).

Definition 3.3.1 Gegenbauer polynomials

✓ 🙂 human-reviewed

#

Gegenbauer polynomials are also called ultraspherical polynomials; see [DLMF, §18.1(ii)]. Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(n\in \mathbb {N}\). Define

\[ C_n^{(\lambda )}(X)=\sum _{k=0}^{\lfloor n/2\rfloor } \frac{(-1)^k(\lambda )_{n-k}}{k!(n-2k)!}(2X)^{n-2k}. \]

Reference: [DLMF, 18.5.10].

Lean Formalisation

def Polynomial.gegenbauer.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) : Polynomial R

Lean definition

/-- Gegenbauer polynomials in DLMF normalisation (DLMF 18.5.10). -/
noncomputable def gegenbauer (lam : R) (n : ℕ) : R[X] :=
  ∑ k ∈ Finset.range (n / 2 + 1),
    C ((-1) ^ k * algebraMap ℚ R (((k.factorial : ℚ) * (n - 2 * k).factorial)⁻¹) *
      (ascPochhammer R (n - k)).eval lam) * (C 2 * X) ^ (n - 2 * k)

Theorem 3.3.2 Gegenbauer degree and leading term

✓ 🙂 human-reviewed

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(n\in \mathbb {N}\). The Gegenbauer polynomial \(C_n^{(\lambda )}(X)\) has degree at most \(n\), and its coefficient of \(X^n\) is

\[ c_n=\frac{2^n(\lambda )_n}{n!}. \]

It has degree exactly \(n\) if and only if \(c_n\ne 0\). In that case, its leading coefficient is \(c_n\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.natDegree_gegenbauer_le.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  (Polynomial.gegenbauer lam n).natDegree ≤ n

Lean proof

/-- The degree is bounded by the index at every parameter (DLMF Table 18.3.1). -/
theorem natDegree_gegenbauer_le (lam : R) (n : ℕ) : (gegenbauer lam n).natDegree ≤ n := by
  unfold gegenbauer
  apply natDegree_sum_le_of_forall_le
  intro k _
  apply (natDegree_C_mul_le _ _).trans
  apply (natDegree_pow_le_of_le _ ((natDegree_C_mul_le _ _).trans natDegree_X_le)).trans
  simp

5 related Lean declarations

theorem Polynomial.degree_gegenbauer_le.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  (Polynomial.gegenbauer lam n).degree ≤ ↑n

Lean proof

/-- The degree bound includes vanishing specialisations (DLMF Table 18.3.1). -/
theorem degree_gegenbauer_le (lam : R) (n : ℕ) : (gegenbauer lam n).degree ≤ n :=
  degree_le_of_natDegree_le (natDegree_gegenbauer_le lam n)

theorem Polynomial.coeff_gegenbauer_self.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  (Polynomial.gegenbauer lam n).coeff n =
    (algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval lam (ascPochhammer R n) * 2 ^ n

Lean proof

/-- The coefficient of `X^n` before imposing nondegeneracy (DLMF Table 18.3.1). -/
theorem coeff_gegenbauer_self (lam : R) (n : ℕ) :
    (gegenbauer lam n).coeff n =
      algebraMap ℚ R ((n.factorial : ℚ)⁻¹) * (ascPochhammer R n).eval lam * 2 ^ n := by
  unfold gegenbauer
  rw [finsetSum_coeff, Finset.sum_eq_single 0]
  · simp only [Nat.mul_zero, Nat.sub_zero, pow_zero, Nat.factorial_zero, Nat.cast_one,
      one_mul, mul_pow, ← C_pow, ← mul_assoc, ← C_mul, coeff_C_mul_X_pow, ite_true]
  · intro k hk hk0
    rw [mul_pow, ← C_pow, ← mul_assoc, ← C_mul, coeff_C_mul_X_pow, ite_eq_right]
    have := Finset.mem_range.mp hk
    omega
  · simp

theorem Polynomial.degree_gegenbauer_eq.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ)
  (h : (algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval lam (ascPochhammer R n) * 2 ^ n ≠ 0) :
  (Polynomial.gegenbauer lam n).degree = ↑n

Lean proof

/-- The nonzero top coefficient is the exact-degree condition
(DLMF Table 18.3.1). -/
theorem degree_gegenbauer_eq (lam : R) (n : ℕ)
    (h : algebraMap ℚ R ((n.factorial : ℚ)⁻¹) *
      (ascPochhammer R n).eval lam * 2 ^ n ≠ 0) : (gegenbauer lam n).degree = n :=
  degree_eq_of_le_of_coeff_ne_zero (degree_gegenbauer_le lam n)
    (by rwa [coeff_gegenbauer_self])

theorem Polynomial.degree_gegenbauer_eq_iff.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  (Polynomial.gegenbauer lam n).degree = ↑n ↔
    (algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval lam (ascPochhammer R n) * 2 ^ n ≠ 0

Lean proof

/-- Exact degree is equivalent to the top coefficient being nonzero
(DLMF Table 18.3.1). -/
theorem degree_gegenbauer_eq_iff (lam : R) (n : ℕ) :
    (gegenbauer lam n).degree = n ↔ algebraMap ℚ R ((n.factorial : ℚ)⁻¹) *
      (ascPochhammer R n).eval lam * 2 ^ n ≠ 0 := by
  constructor
  · intro h
    rw [← coeff_gegenbauer_self]
    exact coeff_ne_zero_of_eq_degree h
  · exact degree_gegenbauer_eq lam n

theorem Polynomial.leadingCoeff_gegenbauer.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ)
  (h : (algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval lam (ascPochhammer R n) * 2 ^ n ≠ 0) :
  (Polynomial.gegenbauer lam n).leadingCoeff =
    (algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval lam (ascPochhammer R n) * 2 ^ n

Lean proof

/-- The leading coefficient at nondegenerate parameters (DLMF Table 18.3.1). -/
theorem leadingCoeff_gegenbauer (lam : R) (n : ℕ)
    (h : algebraMap ℚ R ((n.factorial : ℚ)⁻¹) *
      (ascPochhammer R n).eval lam * 2 ^ n ≠ 0) :
    (gegenbauer lam n).leadingCoeff = algebraMap ℚ R ((n.factorial : ℚ)⁻¹) *
      (ascPochhammer R n).eval lam * 2 ^ n := by
  rw [leadingCoeff, natDegree_eq_of_degree_eq_some (degree_gegenbauer_eq lam n h),
    coeff_gegenbauer_self]

Theorem 3.3.3 Zero Gegenbauer parameter

✓ 🤖

#

For a commutative \(\mathbb {Q}\)-algebra \(R\), \(C_n^{(0)}=0\) for every \(n\ge 1\). The renormalised family is treated after the recurrence (Theorem 3.3.18).

Reference: [DLMF, 18.5.10].

Lean Formalisation

theorem Polynomial.gegenbauer_zero_parameter.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] {n : ℕ} (hn : n ≠ 0) :
  Polynomial.gegenbauer 0 n = 0

Lean proof

/-- Positive-index Gegenbauer polynomials vanish at parameter zero, so this
specialisation is not a polynomial sequence (DLMF 18.5.10). -/
@[simp] theorem gegenbauer_zero_parameter {n : ℕ} (hn : n ≠ 0) :
    gegenbauer (0 : R) n = 0 := by
  unfold gegenbauer
  apply Finset.sum_eq_zero
  intro k hk
  have hnk : n - k ≠ 0 := by
    have := Finset.mem_range.mp hk
    omega
  simp [ascPochhammer_ne_zero_eval_zero R hnk]

Theorem 3.3.4 Gegenbauer derivative

✓ 🙂 human-reviewed

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(n\in \mathbb {N}\). Then

\[ (C_{n+1}^{(\lambda )})'=2\lambda C_n^{(\lambda +1)}. \]

Reference: [DLMF, 18.9.19].

Lean Formalisation

theorem Polynomial.derivative_gegenbauer_succ.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  Polynomial.derivative (Polynomial.gegenbauer lam (n + 1)) = Polynomial.C (2 * lam) * Polynomial.gegenbauer (lam + 1) n

Lean proof

/-- Differentiation raises the Gegenbauer parameter by one (DLMF 18.9.19). -/
theorem derivative_gegenbauer_succ (lam : R) (n : ℕ) :
    derivative (gegenbauer lam (n + 1)) = C (2 * lam) * gegenbauer (lam + 1) n := by
  let c (lam : R) (n k : ℕ) : R := (-1) ^ k *
    algebraMap ℚ R (((k.factorial : ℚ) * (n - 2 * k).factorial)⁻¹) *
    (ascPochhammer R (n - k)).eval lam
  have hrat (k m : ℕ) :
      (m + 1 : ℚ) * (((k.factorial : ℚ) * (m + 1).factorial)⁻¹) =
      (((k.factorial : ℚ) * m.factorial)⁻¹) := by
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
    field_simp
  have hc (k : ℕ) (hk : k ≤ n / 2) :
      c lam (n + 1) k * ((n - 2 * k : ℕ) + 1 : R) = lam * c (lam + 1) n k := by
    have hsub : n + 1 - 2 * k = (n - 2 * k) + 1 := by omega
    have hsub' : n + 1 - k = (n - k) + 1 := by omega
    have hm := congrArg (algebraMap ℚ R) (hrat k (n - 2 * k))
    simp only [map_mul, map_add, map_natCast, map_one] at hm
    dsimp only [c]
    rw [hsub, hsub', ascPochhammer_succ_left, eval_mul, eval_X,
      eval_comp, eval_add, eval_X, eval_one]
    calc
      _ = (-1) ^ k * (((n - 2 * k : ℕ) + 1 : R) * algebraMap ℚ R
          (((k.factorial : ℚ) * ((n - 2 * k) + 1).factorial)⁻¹)) * lam *
          (ascPochhammer R (n - k)).eval (lam + 1) := by ring
      _ = _ := by rw [hm]; ring
  change derivative (∑ k ∈ Finset.range ((n + 1) / 2 + 1),
      C (c lam (n + 1) k) * (C 2 * X) ^ (n + 1 - 2 * k)) =
    C (2 * lam) * ∑ k ∈ Finset.range (n / 2 + 1),
      C (c (lam + 1) n k) * (C 2 * X) ^ (n - 2 * k)
  rw [derivative_sum]
  have hsum :
      (∑ k ∈ Finset.range ((n + 1) / 2 + 1),
        derivative (C (c lam (n + 1) k) * (C 2 * X) ^ (n + 1 - 2 * k))) =
      ∑ k ∈ Finset.range (n / 2 + 1),
        derivative (C (c lam (n + 1) k) * (C 2 * X) ^ (n + 1 - 2 * k)) := by
    by_cases h : (n + 1) / 2 = n / 2
    · rw [h]
    · have hd : (n + 1) / 2 = n / 2 + 1 := by omega
      have hz : n + 1 - 2 * (n / 2 + 1) = 0 := by omega
      rw [hd, Finset.sum_range_succ]
      simp [hz]
  rw [hsum, Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro k hk
  have hk' : k ≤ n / 2 := Nat.le_of_lt_succ (Finset.mem_range.mp hk)
  have he : n + 1 - 2 * k = (n - 2 * k) + 1 := by omega
  rw [derivative_C_mul, he, derivative_pow_succ, derivative_C_mul, derivative_X, mul_one]
  calc
    _ = C (c lam (n + 1) k * ((n - 2 * k : ℕ) + 1 : R)) * C 2 *
        (C 2 * X) ^ (n - 2 * k) := by simp only [C_mul]; ring
    _ = _ := by rw [hc k hk']; simp only [C_mul]; ring

Theorem 3.3.5 Cleared Gegenbauer parameter conversion

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(n\in \mathbb {N}\). Then

\[ (n+\lambda +2)C_{n+2}^{(\lambda )} =\lambda \bigl(C_{n+2}^{(\lambda +1)}-C_n^{(\lambda +1)}\bigr). \]

The initial identities are \(\lambda C_0^{(\lambda )}=\lambda C_0^{(\lambda +1)}\) and \((\lambda +1)C_1^{(\lambda )}=\lambda C_1^{(\lambda +1)}\). No parameter is divided by.

Reference: [DLMF, 18.9.7].

Lean Formalisation

theorem Polynomial.gegenbauer_conversion_zero.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) :
  Polynomial.C lam * Polynomial.gegenbauer lam 0 = Polynomial.C lam * Polynomial.gegenbauer (lam + 1) 0

Lean proof

/-- The constant initial case of parameter conversion (DLMF 18.9.7). -/
theorem gegenbauer_conversion_zero (lam : R) :
    C lam * gegenbauer lam 0 = C lam * gegenbauer (lam + 1) 0 := by simp

2 related Lean declarations

theorem Polynomial.gegenbauer_conversion_one.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) :
  Polynomial.C (lam + 1) * Polynomial.gegenbauer lam 1 = Polynomial.C lam * Polynomial.gegenbauer (lam + 1) 1

Lean proof

/-- The linear initial case of parameter conversion (DLMF 18.9.7). -/
theorem gegenbauer_conversion_one (lam : R) :
    C (lam + 1) * gegenbauer lam 1 = C lam * gegenbauer (lam + 1) 1 := by
  simp only [gegenbauer_one, map_mul]
  ring

theorem Polynomial.gegenbauer_conversion.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  Polynomial.C (↑n + lam + 2) * Polynomial.gegenbauer lam (n + 2) =
    Polynomial.C lam * (Polynomial.gegenbauer (lam + 1) (n + 2) - Polynomial.gegenbauer (lam + 1) n)

Lean proof

/-- The denominator-cleared parameter conversion identity (DLMF 18.9.7). -/
theorem gegenbauer_conversion (lam : R) (n : ℕ) :
    C ((n : R) + lam + 2) * gegenbauer lam (n + 2) =
      C lam * (gegenbauer (lam + 1) (n + 2) - gegenbauer (lam + 1) n) := by
  let : HasUniqueDiv R := HasUniqueDiv.of_module_rat R
  let r (lam : R) (n : ℕ) := C ((n : R) + lam + 2) * gegenbauer lam (n + 2) -
    C lam * (gegenbauer (lam + 1) (n + 2) - gegenbauer (lam + 1) n)
  have hz (lam : R) (n : ℕ) : (r lam n).eval 0 = 0 := by
    obtain ⟨m, hm | hm⟩ := Nat.even_or_odd' n
    · subst n
      have he : 2 * m + 2 = 2 * (m + 1) := by omega
      dsimp only [r]
      rw [he]
      simp only [eval_sub, eval_mul, eval_C, eval_gegenbauer_even_zero]
      have hl : (ascPochhammer R (m + 1)).eval lam =
          lam * (ascPochhammer R m).eval (lam + 1) := by
        rw [ascPochhammer_succ_left, eval_mul, eval_X, eval_comp,
          eval_add, eval_X, eval_one]
      rw [hl, ascPochhammer_succ_eval]
      have hf : (m + 1 : R) * algebraMap ℚ R (((m + 1).factorial : ℚ)⁻¹) =
          algebraMap ℚ R ((m.factorial : ℚ)⁻¹) :=
        Nat.cast_succ_mul_algebraMap_inv_factorial R m
      rw [← hf]
      simp only [Nat.cast_mul, Nat.cast_ofNat, pow_succ]
      ring
    · subst n
      have he : 2 * m + 1 + 2 = 2 * (m + 1) + 1 := by omega
      dsimp only [r]
      rw [he]
      simp only [eval_sub, eval_mul, eval_C, eval_gegenbauer_odd_zero,
        mul_zero, sub_self]
  have finish (p : R[X]) (hd : derivative p = 0) (hv : p.eval 0 = 0) : p = 0 := by
    have hc := eq_C_of_derivative_eq_zero hd
    have he := congrArg (fun q : R[X] => q.eval 0) hc
    simp only [eval_C] at he
    have hcoeff := he.symm.trans hv
    rw [hc, hcoeff, C_0]
  have hzero : ∀ n : ℕ, ∀ lam : R, r lam n = 0 := by
    intro n
    induction n with
    | zero =>
      intro lam
      apply finish _ _ (hz lam 0)
      dsimp only [r]
      simp only [Nat.cast_zero, zero_add]
      simp only [derivative_sub, derivative_C_mul, derivative_gegenbauer_succ,
        gegenbauer_zero, gegenbauer_one, derivative_one, sub_zero]
      simp only [map_mul, map_add, map_ofNat, map_one]
      ring
    | succ n ih =>
      intro lam
      apply finish _ _ (hz lam (n + 1))
      have hprev := ih (lam + 1)
      dsimp only [r] at hprev ⊢
      simp only [derivative_sub, derivative_C_mul, derivative_gegenbauer_succ]
      simp only [Nat.cast_add, Nat.cast_one, map_add, map_mul, map_natCast,
        map_ofNat, map_one] at hprev ⊢
      linear_combination (2 * C lam) * hprev
  exact sub_eq_zero.mp (hzero n lam)

Theorem 3.3.6 Cleared Gegenbauer recurrence

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(n\in \mathbb {N}\). Then

\[ (n+2)C_{n+2}^{(\lambda )}-2(n+\lambda +1)X C_{n+1}^{(\lambda )} +(n+2\lambda )C_n^{(\lambda )}=0. \]

No parameter is divided by.

Reference: [DLMF, Table 18.9.1].

Lean Formalisation

theorem Polynomial.gegenbauer_recurrence.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  Polynomial.C (↑n + 2) * Polynomial.gegenbauer lam (n + 2) -
        Polynomial.C (2 * (↑n + lam + 1)) * Polynomial.X * Polynomial.gegenbauer lam (n + 1) +
      Polynomial.C (↑n + 2 * lam) * Polynomial.gegenbauer lam n =
    0

Lean proof

/-- The denominator-cleared Gegenbauer recurrence (DLMF Table 18.9.1). -/
theorem gegenbauer_recurrence (lam : R) (n : ℕ) :
    C (n + 2 : R) * gegenbauer lam (n + 2) -
      C (2 * ((n : R) + lam + 1)) * X * gegenbauer lam (n + 1) +
      C ((n : R) + 2 * lam) * gegenbauer lam n = 0 := by
  let : HasUniqueDiv R := HasUniqueDiv.of_module_rat R
  let r (lam : R) (n : ℕ) := C (n + 2 : R) * gegenbauer lam (n + 2) -
    C (2 * ((n : R) + lam + 1)) * X * gegenbauer lam (n + 1) +
    C ((n : R) + 2 * lam) * gegenbauer lam n
  have hz (lam : R) (n : ℕ) : (r lam n).eval 0 = 0 := by
    obtain ⟨m, hm | hm⟩ := Nat.even_or_odd' n
    · subst n
      have he : 2 * m + 2 = 2 * (m + 1) := by omega
      dsimp only [r]
      rw [he]
      simp only [eval_add, eval_sub, eval_mul, eval_C, eval_X, mul_zero, zero_mul,
        sub_zero, eval_gegenbauer_even_zero]
      rw [ascPochhammer_succ_eval]
      have hf : (m + 1 : R) * algebraMap ℚ R (((m + 1).factorial : ℚ)⁻¹) =
          algebraMap ℚ R ((m.factorial : ℚ)⁻¹) :=
        Nat.cast_succ_mul_algebraMap_inv_factorial R m
      rw [← hf]
      simp only [Nat.cast_mul, Nat.cast_ofNat, pow_succ]
      ring
    · subst n
      have he : 2 * m + 1 + 2 = 2 * (m + 1) + 1 := by omega
      dsimp only [r]
      rw [he]
      simp only [eval_add, eval_sub, eval_mul, eval_C, eval_X, mul_zero, zero_mul,
        sub_zero, eval_gegenbauer_odd_zero, add_zero]
  have finish (p : R[X]) (hd : derivative p = 0) (hv : p.eval 0 = 0) : p = 0 := by
    have hc := eq_C_of_derivative_eq_zero hd
    have he := congrArg (fun q : R[X] => q.eval 0) hc
    simp only [eval_C] at he
    have hcoeff := he.symm.trans hv
    rw [hc, hcoeff, C_0]
  have hzero : ∀ n : ℕ, ∀ lam : R, r lam n = 0 := by
    intro n
    induction n with
    | zero =>
      intro lam
      apply finish _ _ (hz lam 0)
      dsimp only [r]
      simp only [Nat.cast_zero, zero_add]
      simp only [derivative_add, derivative_sub, derivative_mul, derivative_C,
        derivative_X, derivative_gegenbauer_succ, gegenbauer_zero, gegenbauer_one,
        zero_mul, zero_add, mul_one, add_zero]
      simp only [map_mul, map_add, map_ofNat, map_one]
      ring
    | succ n ih =>
      intro lam
      apply finish _ _ (hz lam (n + 1))
      have hprev := ih (lam + 1)
      have hconv := gegenbauer_conversion lam n
      dsimp only [r] at hprev ⊢
      simp only [derivative_add, derivative_sub, derivative_mul, derivative_C,
        derivative_X, derivative_gegenbauer_succ, zero_mul, zero_add, mul_one]
      simp only [Nat.cast_add, Nat.cast_one, map_add, map_mul, map_natCast,
        map_ofNat, map_one] at hprev hconv ⊢
      linear_combination (2 * C lam) * hprev - 2 * hconv
  exact hzero n lam

Theorem 3.3.7 Gegenbauer differential equation

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(n\in \mathbb {N}\). The Gegenbauer polynomial \(y=C_n^{(\lambda )}(X)\) satisfies

\[ (1-X^2)y''-(2\lambda +1)Xy'+n(n+2\lambda )y=0. \]

Reference: [DLMF, Table 18.8.1].

Lean Formalisation

theorem Polynomial.gegenbauer_differentialEquation.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.derivative (Polynomial.gegenbauer lam n)) -
        Polynomial.C (2 * lam + 1) * Polynomial.X * Polynomial.derivative (Polynomial.gegenbauer lam n) +
      Polynomial.C (↑n * (↑n + 2 * lam)) * Polynomial.gegenbauer lam n =
    0

Lean proof

/-- The Gegenbauer differential equation (DLMF Table 18.8.1). -/
theorem gegenbauer_differentialEquation (lam : R) (n : ℕ) :
    (1 - X ^ 2) * derivative (derivative (gegenbauer lam n)) -
      C (2 * lam + 1) * X * derivative (gegenbauer lam n) +
      C ((n : R) * ((n : R) + 2 * lam)) * gegenbauer lam n = 0 := by
  let : HasUniqueDiv R := HasUniqueDiv.of_module_rat R
  let r (lam : R) (n : ℕ) :=
    (1 - X ^ 2) * derivative (derivative (gegenbauer lam n)) -
      C (2 * lam + 1) * X * derivative (gegenbauer lam n) +
      C ((n : R) * ((n : R) + 2 * lam)) * gegenbauer lam n
  have hz (lam : R) (n : ℕ) : (r lam n).eval 0 = 0 := by
    rcases n with _ | (_ | n)
    · simp [r]
    · simp [r, gegenbauer_one]
    · dsimp only [r]
      simp only [derivative_gegenbauer_succ, derivative_C_mul, eval_add, eval_sub,
        eval_mul, eval_C, eval_one, eval_pow, eval_X, zero_pow (by decide : 2 ≠ 0),
        sub_zero, one_mul, mul_zero, zero_mul]
      obtain ⟨m, hm | hm⟩ := Nat.even_or_odd' n
      · subst n
        have he : 2 * m + 1 + 1 = 2 * (m + 1) := by omega
        rw [he]
        simp only [eval_gegenbauer_even_zero]
        have hl : (ascPochhammer R (m + 1)).eval lam =
            lam * (ascPochhammer R m).eval (lam + 1) := by
          rw [ascPochhammer_succ_left, eval_mul, eval_X, eval_comp,
            eval_add, eval_X, eval_one]
        have hpo : (lam + 1) * (ascPochhammer R m).eval (lam + 1 + 1) =
            (ascPochhammer R m).eval (lam + 1) * (lam + 1 + m) := by
          rw [← ascPochhammer_succ_eval]
          rw [ascPochhammer_succ_left, eval_mul, eval_X, eval_comp,
            eval_add, eval_X, eval_one]
        rw [hl]
        have hf : (m + 1 : R) * algebraMap ℚ R (((m + 1).factorial : ℚ)⁻¹) =
            algebraMap ℚ R ((m.factorial : ℚ)⁻¹) :=
          Nat.cast_succ_mul_algebraMap_inv_factorial R m
        rw [← hf]
        simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_one, pow_succ]
        linear_combination (4 * lam * (-1 : R) ^ m * ((m + 1 : R) *
          algebraMap ℚ R (((m + 1).factorial : ℚ)⁻¹))) * hpo
      · subst n
        have he : 2 * m + 1 + 1 + 1 = 2 * (m + 1) + 1 := by omega
        rw [he]
        simp only [eval_gegenbauer_odd_zero, mul_zero, add_zero]
  have hzero : ∀ n : ℕ, ∀ lam : R, r lam n = 0 := by
    intro n
    induction n with
    | zero => intro lam; simp [r]
    | succ n ih =>
      intro lam
      have hd : derivative (r lam (n + 1)) = 0 := by
        have hi := ih (lam + 1)
        dsimp only [r] at hi ⊢
        simp only [derivative_add, derivative_sub, derivative_mul, derivative_one,
          derivative_X_pow, derivative_X, derivative_C, zero_mul, zero_add,
          zero_sub, mul_one]
        rw [derivative_gegenbauer_succ, derivative_C_mul, derivative_C_mul]
        simp only [Nat.cast_add, Nat.cast_one, map_add, map_mul, map_natCast,
          map_ofNat, map_one] at hi ⊢
        linear_combination (2 * C lam) * hi
      have hc := eq_C_of_derivative_eq_zero hd
      have he := congrArg (fun p : R[X] => p.eval 0) hc
      simp only [eval_C] at he
      have hcoeff := he.symm.trans (hz lam (n + 1))
      rw [hc, hcoeff, C_0]
  exact hzero n lam

Theorem 3.3.8 Gegenbauer endpoint value

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(n\in \mathbb {N}\). Then \(C_n^{(\lambda )}(1)=(2\lambda )_n/n!\).

Reference: [DLMF, Table 18.6.1].

Lean Formalisation

theorem Polynomial.eval_gegenbauer_one.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  Polynomial.eval 1 (Polynomial.gegenbauer lam n) =
    (algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval (2 * lam) (ascPochhammer R n)

Lean proof

/-- The Gegenbauer value at one, including exceptional parameters (DLMF Table 18.6.1). -/
theorem eval_gegenbauer_one {R : Type*} [CommRing R] [Algebra ℚ R]
    (lam : R) (n : ℕ) :
    (gegenbauer lam n).eval 1 = algebraMap ℚ R ((n.factorial : ℚ)⁻¹) *
      (ascPochhammer R n).eval (2 * lam) := by
  have h := eval_gegenbauer_one_domain (X : ℚ[X]) n
  let f : ℚ[X] →ₐ[ℚ] R := aeval lam
  have hm := congrArg f h
  have hg := map_gegenbauer f X n
  have hj := map_jacobi f (2 * X - 1) 0 n
  have hev (p : ℚ[X][X]) : f (p.eval 1) = (p.map f.toRingHom).eval 1 := by
    rw [eval_map, eval₂_at_one]; rfl
  rw [hev, hev, hg, hj] at hm
  simpa [f, eval_jacobi_one, map_ofNat] using hm

Theorem 3.3.9 Gegenbauer parity

✓ 🙂 human-reviewed

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(n\in \mathbb {N}\). Then \(C_n^{(\lambda )}(-X)=(-1)^n C_n^{(\lambda )}(X)\).

Reference: [DLMF, Table 18.6.1].

Lean Formalisation

theorem Polynomial.gegenbauer_comp_neg_X.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  (Polynomial.gegenbauer lam n).comp (-Polynomial.X) = Polynomial.C ((-1) ^ n) * Polynomial.gegenbauer lam n

Lean proof

/-- Gegenbauer parity holds at every parameter (DLMF Table 18.6.1). -/
theorem gegenbauer_comp_neg_X (lam : R) (n : ℕ) :
    (gegenbauer lam n).comp (-X) = C ((-1 : R) ^ n) * gegenbauer lam n := by
  unfold gegenbauer
  rw [sum_comp, Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro k hk
  have hk' : 2 * k ≤ n := by
    have := Finset.mem_range.mp hk
    omega
  have hs : (-1 : R[X]) ^ (n - 2 * k) = (-1 : R[X]) ^ n := by
    nth_rw 2 [← Nat.sub_add_cancel hk']
    rw [pow_add, pow_mul]
    simp
  simp only [mul_comp, C_comp, pow_comp, X_comp]
  rw [show C (2 : R) * (-X) = -(C 2 * X) by ring]
  rw [neg_pow (C (2 : R) * X), hs]
  simp only [map_pow, map_neg, map_one]
  ring

1 related Lean declaration

theorem Polynomial.eval_gegenbauer_neg.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam x : R) (n : ℕ) :
  Polynomial.eval (-x) (Polynomial.gegenbauer lam n) = (-1) ^ n * Polynomial.eval x (Polynomial.gegenbauer lam n)

Lean proof

/-- Evaluation form of the parity identity (DLMF Table 18.6.1). -/
theorem eval_gegenbauer_neg (lam x : R) (n : ℕ) :
    (gegenbauer lam n).eval (-x) = (-1 : R) ^ n * (gegenbauer lam n).eval x := by
  have h := congrArg (fun p : R[X] => p.eval x) (gegenbauer_comp_neg_X lam n)
  simpa only [eval_comp, eval_neg, eval_X, eval_mul, eval_C] using h

Theorem 3.3.10 Gegenbauer–Jacobi bridge

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(n\in \mathbb {N}\). Then

\[ (\lambda +\tfrac 12)_n C_n^{(\lambda )} =(2\lambda )_n P_n^{(\lambda -1/2,\lambda -1/2)}. \]

No parameter factor is cancelled, so the identity includes singular specialisations.

Reference: [DLMF, 18.7.1].

Lean Formalisation

theorem Polynomial.gegenbauer_jacobi.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) :
  Polynomial.C (Polynomial.eval (lam + (algebraMap ℚ R) (1 / 2)) (ascPochhammer R n)) * Polynomial.gegenbauer lam n =
    Polynomial.C (Polynomial.eval (2 * lam) (ascPochhammer R n)) *
      Polynomial.jacobi (lam - (algebraMap ℚ R) (1 / 2)) (lam - (algebraMap ℚ R) (1 / 2)) n

Lean proof

/-- The cleared Gegenbauer--Jacobi bridge at every parameter (DLMF 18.7.1). -/
theorem gegenbauer_jacobi {R : Type*} [CommRing R] [Algebra ℚ R]
    (lam : R) (n : ℕ) :
    C ((ascPochhammer R n).eval (lam + algebraMap ℚ R (1 / 2))) * gegenbauer lam n =
      C ((ascPochhammer R n).eval (2 * lam)) *
        jacobi (lam - algebraMap ℚ R (1 / 2)) (lam - algebraMap ℚ R (1 / 2)) n := by
  have h := gegenbauer_jacobi_of_nonzero (X : ℚ[X]) n (fun k hk ↦ by
    have hc := congrArg (fun p : ℚ[X] ↦ p.coeff 1) hk
    norm_num [coeff_add, coeff_sub, coeff_natCast_ite, coeff_one, algebraMap_apply] at hc)
  let f : ℚ[X] →ₐ[ℚ] R := aeval lam
  have hp (k : ℕ) (x : ℚ[X]) : f ((ascPochhammer ℚ[X] k).eval x) =
      (ascPochhammer R k).eval (f x) := by
    rw [← ascPochhammer_map f.toRingHom, eval_map]
    exact (eval₂_at_apply f.toRingHom x).symm
  have hm := congrArg (Polynomial.map f.toRingHom) h
  simp only [Polynomial.map_mul, Polynomial.map_C, map_gegenbauer, map_jacobi] at hm
  simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, hp, map_add, map_sub,
    map_mul, map_ofNat, AlgHom.commutes] at hm
  simpa [f] using hm

Theorem 3.3.11 Gegenbauer hypergeometric representations

✓ 🤖

#

Let \(\lambda \) and \(x\) be real or complex and \(n\in \mathbb {N}\). If \((\lambda +\tfrac 12)_n\ne 0\), then

\[ C_n^{(\lambda )}(x)=\frac{(2\lambda )_n}{n!}\, {}_2F_1\! \left(-n,n+2\lambda ;\lambda +\tfrac 12;\frac{1-x}2\right). \]

If \(x\ne 0\) and \((1-\lambda -n)_{\lfloor n/2\rfloor }\ne 0\), then

\[ C_n^{(\lambda )}(x)=(2x)^n\frac{(\lambda )_n}{n!}\, {}_2F_1\! \left(-\tfrac n2,\tfrac {1-n}2;1-\lambda -n;\frac1{x^2}\right). \]

Here \({}_2F_1\) is the Gauss series of Definition 1.2.6. The conditions exclude exactly the denominator factors that occur. The second condition is satisfied at \(\lambda =0\) and \(\lambda =1\) for every \(n\).

Reference: [DLMF, 18.5.9 and 18.5.10].

Lean Formalisation

theorem Polynomial.eval_gegenbauer_eq_ordinaryHypergeometric.{u_1} {𝕂 : Type u_1} [RCLike 𝕂] (lam x : 𝕂) (n : ℕ)
  (hc : Polynomial.eval (lam + 1 / 2) (ascPochhammer 𝕂 n) ≠ 0) :
  Polynomial.eval x (Polynomial.gegenbauer lam n) =
    Polynomial.eval (2 * lam) (ascPochhammer 𝕂 n) / ↑n.factorial *
      ordinaryHypergeometricOn (GaussParameters.ofTerminating (-↑n) (↑n + 2 * lam) (lam + 1 / 2) n ⋯ hc)
        (GaussSeriesPoint.ofTerminating (GaussParameters.ofTerminating (-↑n) (↑n + 2 * lam) (lam + 1 / 2) n ⋯ hc) n ⋯
          ((1 - x) / 2))

Lean proof

/-- Gegenbauer's classical terminating Gauss representation. -/
theorem eval_gegenbauer_eq_ordinaryHypergeometric {𝕂 : Type*} [RCLike 𝕂]
    (lam x : 𝕂) (n : ℕ) (hc : (ascPochhammer 𝕂 n).eval (lam + 1 / 2) ≠ 0) :
    (gegenbauer lam n).eval x = (ascPochhammer 𝕂 n).eval (2 * lam) / n.factorial *
      ordinaryHypergeometricOn (GaussParameters.ofTerminating (-(n : 𝕂)) (n + 2 * lam) (lam + 1 / 2) n (Or.inl rfl) hc)
        (.ofTerminating _ n (Or.inl rfl) ((1 - x) / 2)) := by
  have e1 : lam - 1 / 2 + 1 = lam + 1 / 2 := by ring
  have e2 : (n : 𝕂) + (lam - 1 / 2) + (lam - 1 / 2) + 1 = n + 2 * lam := by ring
  have hb := congrArg (eval x) (gegenbauer_jacobi lam n)
  have hj := eval_jacobi_eq_ordinaryHypergeometric (lam - 1 / 2) (lam - 1 / 2) x n
    (by rwa [e1])
  rw [ordinaryHypergeometricOn_terminating] at hj ⊢
  simp only [ordinaryHypergeometricCoefficientOn, GaussParameters.ofTerminating] at hj ⊢
  have h12 : algebraMap ℚ 𝕂 (1 / 2) = 1 / 2 := by simp
  simp only [eval_mul, eval_C, h12] at hb
  simp only [e1, e2] at hj
  rw [hj] at hb
  apply mul_left_cancel₀ hc
  rw [hb]
  ring_nf

1 related Lean declaration

theorem Polynomial.eval_gegenbauer_eq_ordinaryHypergeometric_inv_sq.{u_1} {𝕂 : Type u_1} [RCLike 𝕂] (lam : 𝕂) (x : 𝕂ˣ) (n : ℕ)
  (hc : Polynomial.eval (1 - lam - ↑n) (ascPochhammer 𝕂 (n / 2)) ≠ 0) :
  Polynomial.eval (↑x) (Polynomial.gegenbauer lam n) =
    (2 * ↑x) ^ n * (Polynomial.eval lam (ascPochhammer 𝕂 n) / ↑n.factorial) *
      ordinaryHypergeometricOn (GaussParameters.quadratic n (1 - lam - ↑n) hc)
        (GaussSeriesPoint.ofTerminating (GaussParameters.quadratic n (1 - lam - ↑n) hc) (n / 2) ⋯ (↑x ^ 2)⁻¹)

Lean proof

/-- Gegenbauer's classical inverse-square representation on its exact stated domain. -/
theorem eval_gegenbauer_eq_ordinaryHypergeometric_inv_sq {𝕂 : Type*} [RCLike 𝕂]
    (lam : 𝕂) (x : 𝕂ˣ) (n : ℕ)
    (hc : (ascPochhammer 𝕂 (n / 2)).eval (1 - lam - n) ≠ 0) :
    (gegenbauer lam n).eval x.val =
      (2 * x.val) ^ n * ((ascPochhammer 𝕂 n).eval lam / n.factorial) *
        ordinaryHypergeometricOn (GaussParameters.quadratic n (1 - lam - n) hc)
          (.ofTerminating _ (n / 2) (GaussParameters.quadratic_has_termination n _ _) (x.val ^ 2)⁻¹) := by
  have hq := two_mul_pow_mul_ordinaryHypergeometric_inv_sq n ⟨1 - lam - n, hc⟩ x
  rw [Fin.sum_univ_eq_sum_range (fun k : ℕ ↦
    (n.factorial : 𝕂) / (k.factorial * (n - 2 * k).factorial) *
      ((ascPochhammer 𝕂 k).eval (1 - lam - n))⁻¹ * (2 * x.val) ^ (n - 2 * k))
      (n / 2 + 1)] at hq

  rw [mul_comm ((2 * x.val) ^ n), mul_assoc, hq,
    Finset.mul_sum, gegenbauer, eval_finsetSum]
  refine Finset.sum_congr rfl fun k hk ↦ ?_
  have hk : 2 * k ≤ n := by
    have := Finset.mem_range.mp hk
    omega
  -- `(λ)_n = (λ)_{n-k} (λ+n-k)_k` and `(1-λ-n)_k = (-1)^k (λ+n-k)_k`.
  have hsplit := congrArg (eval lam) (ascPochhammer_mul 𝕂 (n - k) k)
  simp only [eval_mul, eval_comp, eval_add, eval_X, eval_natCast,
    Nat.sub_add_cancel (by omega : k ≤ n)] at hsplit
  have hrefl : (ascPochhammer 𝕂 k).eval (1 - lam - n) =
      (-1) ^ k * (ascPochhammer 𝕂 k).eval (lam + (n - k : ℕ)) := by
    rw [show (1 : 𝕂) - lam - n = -(lam + n - 1) by ring,
      ascPochhammer_eval_neg_eq_descPochhammer, descPochhammer_eval_eq_ascPochhammer]
    congr 2
    push_cast [show k ≤ n by omega]
    ring
  have hck : (ascPochhammer 𝕂 k).eval (1 - lam - n) ≠ 0 := by
    intro hz
    apply hc
    have hm := congrArg (eval (1 - lam - n)) (ascPochhammer_mul 𝕂 k (n / 2 - k))
    simp only [eval_mul, eval_comp, eval_add, eval_X, eval_natCast, hz, zero_mul,
      Nat.add_sub_cancel' (by omega : k ≤ n / 2)] at hm
    exact hm.symm
  have hkf : (k.factorial : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero k)
  have hnf : ((n - 2 * k).factorial : 𝕂) ≠ 0 :=
    Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
  have hnn : (n.factorial : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)
  rw [hrefl] at hck ⊢
  simp only [eval_mul, eval_C, eval_pow, eval_X, map_inv₀, map_mul, map_natCast,
    ← hsplit]
  have hck' : (ascPochhammer 𝕂 k).eval (lam + (n - k : ℕ)) ≠ 0 := by
    intro hz; apply hck; rw [hz, mul_zero]
  have hs : ((-1 : 𝕂) ^ k)⁻¹ = (-1) ^ k := by rw [← inv_pow, inv_neg, inv_one]
  rw [mul_inv ((-1 : 𝕂) ^ k), hs]
  field_simp

Low degrees, parameter limits and hypergeometric reindexing

Theorem 3.3.12 Low degrees and parameter substitution

✓ 🤖

#

For a commutative \(\mathbb {Q}\)-algebra \(R\) and \(\lambda \in R\), \(C_0^{(\lambda )}=1\) and \(C_1^{(\lambda )}=2\lambda X\). For every \(\mathbb {Q}\)-algebra homomorphism \(f:R\to S\) and \(n\in \mathbb {N}\), applying \(f\) to the coefficients of \(C_n^{(\lambda )}\) gives \(C_n^{(f(\lambda ))}\).

Reference: [DLMF, 18.5.10].

Lean Formalisation

theorem Polynomial.gegenbauer_zero.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) : Polynomial.gegenbauer lam 0 = 1

Lean proof

/-- The constant member is one (DLMF 18.5.10). -/
@[simp] theorem gegenbauer_zero (lam : R) : gegenbauer lam 0 = 1 := by
  simp [gegenbauer]

2 related Lean declarations

theorem Polynomial.gegenbauer_one.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) :
  Polynomial.gegenbauer lam 1 = Polynomial.C (2 * lam) * Polynomial.X

Lean proof

/-- The degree-one member is `2 lam X` (DLMF 18.5.10). -/
@[simp] theorem gegenbauer_one (lam : R) : gegenbauer lam 1 = C (2 * lam) * X := by
  simp [gegenbauer, map_mul]
  ring

theorem Polynomial.map_gegenbauer.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [Algebra ℚ R] [CommRing S] [Algebra ℚ S]
  (f : R →ₐ[ℚ] S) (lam : R) (n : ℕ) :
  Polynomial.map f.toRingHom (Polynomial.gegenbauer lam n) = Polynomial.gegenbauer (f lam) n

Lean proof

/-- Gegenbauer polynomials commute with rational algebra maps (DLMF 18.5.10). -/
theorem map_gegenbauer {R S : Type*} [CommRing R] [Algebra ℚ R]
    [CommRing S] [Algebra ℚ S] (f : R →ₐ[ℚ] S) (lam : R) (n : ℕ) :
    (gegenbauer lam n).map f.toRingHom = gegenbauer (f lam) n := by
  have hp (k : ℕ) (x : R) : f ((ascPochhammer R k).eval x) =
      (ascPochhammer S k).eval (f x) := by
    rw [← ascPochhammer_map f.toRingHom, eval_map]
    exact (eval₂_at_apply f.toRingHom x).symm
  simp only [gegenbauer, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C,
    Polynomial.map_pow, Polynomial.map_neg, Polynomial.map_one, Polynomial.map_ofNat, map_X, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
    map_mul, map_pow, map_neg, map_one, map_ofNat, hp, AlgHom.commutes]

Theorem 3.3.13 Gegenbauer values at zero

✓ 🙂 human-reviewed

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\lambda \in R\), and let \(m\in \mathbb {N}\). Then

\[ C_{2m}^{(\lambda )}(0)=(-1)^m\frac{(\lambda )_m}{m!},\qquad C_{2m+1}^{(\lambda )}(0)=0. \]

Reference: [DLMF, Table 18.6.1].

Lean Formalisation

theorem Polynomial.eval_gegenbauer_even_zero.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (m : ℕ) :
  Polynomial.eval 0 (Polynomial.gegenbauer lam (2 * m)) =
    (-1) ^ m * (algebraMap ℚ R) (↑m.factorial)⁻¹ * Polynomial.eval lam (ascPochhammer R m)

Lean proof

/-- Even-index values at zero (DLMF Table 18.6.1). -/
theorem eval_gegenbauer_even_zero (lam : R) (m : ℕ) :
    (gegenbauer lam (2 * m)).eval 0 = (-1 : R) ^ m *
      algebraMap ℚ R ((m.factorial : ℚ)⁻¹) * (ascPochhammer R m).eval lam := by
  unfold gegenbauer
  rw [eval_finsetSum, Finset.sum_eq_single m]
  · simp [show 2 * m - m = m by omega]
  · intro k hk hkm
    have he : 2 * m - 2 * k ≠ 0 := by
      have := Finset.mem_range.mp hk
      omega
    simp [he]
  · simp

1 related Lean declaration

theorem Polynomial.eval_gegenbauer_odd_zero.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (m : ℕ) :
  Polynomial.eval 0 (Polynomial.gegenbauer lam (2 * m + 1)) = 0

Lean proof

/-- Odd-index values at zero (DLMF Table 18.6.1). -/
@[simp] theorem eval_gegenbauer_odd_zero (lam : R) (m : ℕ) :
    (gegenbauer lam (2 * m + 1)).eval 0 = 0 := by
  unfold gegenbauer
  rw [eval_finsetSum]
  apply Finset.sum_eq_zero
  intro k hk
  have he : 2 * m + 1 - 2 * k ≠ 0 := by
    have := Finset.mem_range.mp hk
    omega
  simp [he]

Definition 3.3.14 Reduced Gegenbauer polynomials

✓ 🤖

#

For a commutative \(\mathbb {Q}\)-algebra \(R\) and \(\lambda \in R\), normalize \(R_0^{(\lambda )}=1\). For \(n\ge 1\), define

\[ R_n^{(\lambda )}(X)=\sum _{k=0}^{\lfloor n/2\rfloor } \frac{(-1)^k(\lambda +1)_{n-k-1}}{k!(n-2k)!}(2X)^{n-2k}. \]

Reference: [DLMF, 18.5.10], [DLMF, §18.7(iii)].

Lean Formalisation

def Polynomial.gegenbauerReduced.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) (n : ℕ) : Polynomial R

Lean definition

/-- The Gegenbauer sum (DLMF 18.5.10) with one factor `λ` removed from each rising
factorial, `(λ)_{n-k} = λ (λ + 1)_{n-k-1}` (DLMF 18.7(iii)). The value at `n = 0` is
the normalization `R₀ = 1`. The identity `Cₙ = λ Rₙ` applies only in positive degree. -/
noncomputable def gegenbauerReduced (lam : R) (n : ℕ) : R[X] :=
  ∑ k ∈ Finset.range (n / 2 + 1),
    C ((-1) ^ k * algebraMap ℚ R (((k.factorial : ℚ) * (n - 2 * k).factorial)⁻¹) *
      (ascPochhammer R (n - k - 1)).eval (lam + 1)) * (C 2 * X) ^ (n - 2 * k)

Theorem 3.3.15 Factoring out the parameter

✓ 🤖

#

For a commutative \(\mathbb {Q}\)-algebra \(R\) and \(\lambda \in R\), \(R_0^{(\lambda )}=1\), and \(C_n^{(\lambda )}=\lambda R_n^{(\lambda )}\) for \(n\ge 1\). For every \(n\ge 0\) and every \(\mathbb {Q}\)-algebra homomorphism \(f:R\to S\), applying \(f\) to the coefficients of \(R_n^{(\lambda )}\) gives \(R_n^{(f(\lambda ))}\).

Reference: [DLMF, 18.5.10].

Lean Formalisation

theorem Polynomial.gegenbauerReduced_zero.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) :
  Polynomial.gegenbauerReduced lam 0 = 1

Lean proof

/-- The degree-zero normalization of the reduced family is one. -/
@[simp] theorem gegenbauerReduced_zero (lam : R) : gegenbauerReduced lam 0 = 1 := by
  simp only [gegenbauerReduced, Nat.zero_div, zero_add, Finset.sum_range_one,
    pow_zero, Nat.factorial_zero, Nat.cast_one, mul_one, Nat.zero_sub,
    inv_one, map_one, ascPochhammer_zero, eval_one]

2 related Lean declarations

theorem Polynomial.gegenbauer_eq_C_mul_gegenbauerReduced.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) {n : ℕ}
  (hn : n ≠ 0) : Polynomial.gegenbauer lam n = Polynomial.C lam * Polynomial.gegenbauerReduced lam n

Lean proof

/-- Positive-degree Gegenbauer polynomials are `λ` times the reduced polynomials
(DLMF 18.5.10, 18.7(iii)). -/
theorem gegenbauer_eq_C_mul_gegenbauerReduced (lam : R) {n : ℕ} (hn : n ≠ 0) :
    gegenbauer lam n = C lam * gegenbauerReduced lam n := by
  unfold gegenbauer gegenbauerReduced
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun k hk ↦ ?_
  have hnk : n - k = n - k - 1 + 1 := by
    have := Finset.mem_range.mp hk
    omega
  conv_lhs => rw [hnk]
  rw [ascPochhammer_succ_left, eval_mul, eval_X, eval_comp, eval_add, eval_X, eval_one]
  simp only [C_mul]
  ring

theorem Polynomial.map_gegenbauerReduced.{u_1, u_2} {R : Type u_1} [CommRing R] [Algebra ℚ R] {S : Type u_2} [CommRing S]
  [Algebra ℚ S] (f : R →ₐ[ℚ] S) (lam : R) (n : ℕ) :
  Polynomial.map f.toRingHom (Polynomial.gegenbauerReduced lam n) = Polynomial.gegenbauerReduced (f lam) n

Lean proof

/-- Reduced Gegenbauer polynomials commute with rational algebra maps (DLMF 18.5.10). -/
theorem map_gegenbauerReduced {S : Type*} [CommRing S] [Algebra ℚ S] (f : R →ₐ[ℚ] S)
    (lam : R) (n : ℕ) :
    (gegenbauerReduced lam n).map f.toRingHom = gegenbauerReduced (f lam) n := by
  have hp (k : ℕ) (x : R) : f ((ascPochhammer R k).eval x) =
      (ascPochhammer S k).eval (f x) := by
    rw [← ascPochhammer_map f.toRingHom, eval_map]
    exact (eval₂_at_apply f.toRingHom x).symm
  simp only [gegenbauerReduced, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C,
    Polynomial.map_pow, Polynomial.map_neg, Polynomial.map_one, Polynomial.map_ofNat, map_X,
    AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, map_mul, map_pow, map_neg, map_one,
    map_ofNat, map_add, hp,
    AlgHom.commutes]

Theorem 3.3.16 Reduced Gegenbauer recurrence

✓ 🤖

#

For a commutative \(\mathbb {Q}\)-algebra \(R\), \(\lambda \in R\) and \(n\ge 1\),

\[ (n+2)R_{n+2}^{(\lambda )}-2(n+\lambda +1)XR_{n+1}^{(\lambda )} +(n+2\lambda )R_n^{(\lambda )}=0. \]

Reference: [DLMF, Table 18.9.1].

Lean Formalisation

theorem Polynomial.gegenbauerReduced_recurrence.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (lam : R) {n : ℕ} (hn : n ≠ 0) :
  Polynomial.C (↑n + 2) * Polynomial.gegenbauerReduced lam (n + 2) -
        Polynomial.C (2 * (↑n + lam + 1)) * Polynomial.X * Polynomial.gegenbauerReduced lam (n + 1) +
      Polynomial.C (↑n + 2 * lam) * Polynomial.gegenbauerReduced lam n =
    0

Lean proof

/-- The Gegenbauer recurrence divided by `λ`, valid from degree one
(DLMF Table 18.9.1, 18.7(iii)). -/
theorem gegenbauerReduced_recurrence (lam : R) {n : ℕ} (hn : n ≠ 0) :
    C (n + 2 : R) * gegenbauerReduced lam (n + 2) -
      C (2 * ((n : R) + lam + 1)) * X * gegenbauerReduced lam (n + 1) +
      C ((n : R) + 2 * lam) * gegenbauerReduced lam n = 0 := by
  have h := congrArg (Polynomial.map (aeval lam).toRingHom)
    (gegenbauerReduced_recurrence_generic hn)
  have hm (m : ℕ) := map_gegenbauerReduced (aeval lam) (X : ℚ[X]) m
  simp only [AlgHom.toRingHom_eq_coe, aeval_X] at hm h
  simpa only [Polynomial.map_add, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_C,
    map_X, Polynomial.map_zero, Polynomial.map_natCast, Polynomial.map_ofNat,
    Polynomial.map_one, hm, AlgHom.coe_toRingHom, map_add, map_mul, map_natCast, map_ofNat,
    map_one, aeval_X] using h

Theorem 3.3.17 Chebyshev T at parameter zero

✓ 🤖

#

For a commutative \(\mathbb {Q}\)-algebra \(R\) and \(n\ge 1\), \(nR_n^{(0)}=2T_n\). When \(n\) is invertible, \(R_n^{(0)}=(2/n)T_n\).

Reference: [DLMF, 18.1.1].

Lean Formalisation

theorem Polynomial.natCast_mul_gegenbauerReduced_zero.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] {n : ℕ} (hn : n ≠ 0) :
  ↑n * Polynomial.gegenbauerReduced 0 n = 2 * Polynomial.Chebyshev.T R ↑n

Lean proof

/-- At parameter zero, `n R_n^{(0)} = 2 T_n` for `n ≥ 1`. This is the Chebyshev T
normalisation `C_n^{(0)} = (2/n) T_n` of DLMF 18.1.1 (see DLMF 18.7(iii)). -/
theorem natCast_mul_gegenbauerReduced_zero {n : ℕ} (hn : n ≠ 0) :
    (n : R[X]) * gegenbauerReduced (0 : R) n = 2 * Chebyshev.T R n := by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
  let f : ℚ →ₐ[ℚ] R := Algebra.ofId ℚ R
  have h := congrArg (Polynomial.map f.toRingHom) (natCast_mul_gegenbauerReduced_zero_rat m)
  simpa only [Polynomial.map_mul, Polynomial.map_natCast, Polynomial.map_ofNat,
    map_gegenbauerReduced, map_zero, Chebyshev.map_T] using h

Theorem 3.3.18 Gegenbauer polynomials divided by the parameter

✓ 🤖

#

For \(n\ge 1\) and \(x\in \mathbb {R}\), \(\lambda \mapsto R_n^{(\lambda )}(x)\) is continuous on \(\mathbb {R}\), and

\[ \lim _{\lambda \to 0,\ \lambda \ne 0}\frac{C_n^{(\lambda )}(x)}{\lambda } =\frac2n\, T_n(x). \]

Reference: [DLMF, §18.7(iii)].

Lean Formalisation

theorem Polynomial.continuous_eval_gegenbauerReduced (n : ℕ) (x : ℝ) :
  Continuous fun lam => Polynomial.eval x (Polynomial.gegenbauerReduced lam n)

Lean proof

/-- Reduced Gegenbauer polynomials depend continuously on a real parameter
(DLMF 18.5.10). -/
theorem continuous_eval_gegenbauerReduced (n : ℕ) (x : ℝ) :
    Continuous fun lam : ℝ ↦ (gegenbauerReduced lam n).eval x := by
  simp only [gegenbauerReduced, eval_finsetSum, eval_mul, eval_C, eval_pow, eval_X]
  fun_prop

1 related Lean declaration

theorem Polynomial.tendsto_eval_gegenbauer_div_nhdsNE_zero {n : ℕ} (hn : n ≠ 0) (x : ℝ) :
  Filter.Tendsto (fun lam => Polynomial.eval x (Polynomial.gegenbauer lam n) / lam) (nhdsWithin 0 {0}ᶜ)
    (nhds (2 / ↑n * Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)))

Lean proof

/-- Divided by `λ`, real Gegenbauer polynomials tend to `(2/n) T_n` as `λ → 0`,
`λ ≠ 0`, for `n ≥ 1` (DLMF 18.1.1, 18.7(iii)). -/
theorem tendsto_eval_gegenbauer_div_nhdsNE_zero {n : ℕ} (hn : n ≠ 0) (x : ℝ) :
    Tendsto (fun lam : ℝ ↦ (gegenbauer lam n).eval x / lam) (𝓝[≠] 0)
      (𝓝 (2 / n * (Chebyshev.T ℝ n).eval x)) := by
  have h0 : (gegenbauerReduced (0 : ℝ) n).eval x = 2 / n * (Chebyshev.T ℝ n).eval x := by
    have h := congrArg (eval x) (natCast_mul_gegenbauerReduced_zero (R := ℝ) hn)
    simp only [eval_mul, eval_natCast, eval_ofNat] at h
    have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn
    field_simp
    linarith
  rw [← h0]
  refine ((continuous_eval_gegenbauerReduced n x).tendsto 0).mono_left nhdsWithin_le_nhds
    |>.congr' ?_
  filter_upwards [self_mem_nhdsWithin] with lam hlam
  rw [gegenbauer_eq_C_mul_gegenbauerReduced lam hn, eval_mul, eval_C,
    mul_div_cancel_left₀ _ hlam]

Theorem 3.3.19 Quadratic Gauss reindexing

✓ 🤖

#

Over a characteristic-zero field, \(4^k(a)_k(a+\tfrac 12)_k=(2a)_{2k}\) for all \(a\) and \(k\in \mathbb {N}\). For real or complex \(c\), \(x\ne 0\), and \(n\in \mathbb {N}\) with \((c)_{\lfloor n/2\rfloor }\ne 0\),

\[ (2x)^n\, {}_2F_1\! \left(-\tfrac n2,\tfrac {1-n}2;c;\frac1{x^2}\right) =\sum _{k=0}^{\lfloor n/2\rfloor }\frac{n!}{k!\, (n-2k)!\, (c)_k}(2x)^{n-2k}, \]

where \({}_2F_1\) is the Gauss series of Definition 1.2.6. Every denominator factor in the finite sum is nonzero.

Reference: [DLMF, 5.2.8 and 15.2.1].

Lean Formalisation

theorem Polynomial.four_pow_mul_ascPochhammer_eval_mul_eval_add_half.{u_1} {K : Type u_1} [Field K] [CharZero K] (a : K)
  (k : ℕ) :
  4 ^ k * (Polynomial.eval a (ascPochhammer K k) * Polynomial.eval (a + 1 / 2) (ascPochhammer K k)) =
    Polynomial.eval (2 * a) (ascPochhammer K (2 * k))

Lean proof

/-- Legendre duplication for rising factorials, with denominators cleared:
`4^k (a)_k (a + 1/2)_k = (2a)_{2k}` (DLMF 5.2.8). -/
theorem four_pow_mul_ascPochhammer_eval_mul_eval_add_half {K : Type*} [Field K]
    [CharZero K] (a : K) (k : ℕ) :
    4 ^ k * ((ascPochhammer K k).eval a * (ascPochhammer K k).eval (a + 1 / 2)) =
      (ascPochhammer K (2 * k)).eval (2 * a) := by
  induction k with
  | zero => simp
  | succ k ih =>
    rw [show 2 * (k + 1) = 2 * k + 1 + 1 by ring, ascPochhammer_succ_eval,
      ascPochhammer_succ_eval, ascPochhammer_succ_eval, ascPochhammer_succ_eval, ← ih]
    push_cast
    ring

1 related Lean declaration

theorem Polynomial.two_mul_pow_mul_ordinaryHypergeometric_inv_sq.{u_1} {𝕂 : Type u_1} [RCLike 𝕂] (n : ℕ)
  (c : { c // Polynomial.eval c (ascPochhammer 𝕂 (n / 2)) ≠ 0 }) (x : 𝕂ˣ) :
  (2 * ↑x) ^ n *
      ordinaryHypergeometricOn (GaussParameters.quadratic n ↑c ⋯)
        (GaussSeriesPoint.ofTerminating (GaussParameters.quadratic n ↑c ⋯) (n / 2) ⋯ (↑x ^ 2)⁻¹) =
    ∑ k,
      ↑n.factorial / (↑(↑k).factorial * ↑(n - 2 * ↑k).factorial) * (Polynomial.eval (↑c) (ascPochhammer 𝕂 ↑k))⁻¹ *
        (2 * ↑x) ^ (n - 2 * ↑k)

Lean proof

/-- The quadratic reindexing uses only nonzero arguments and finite admissible denominators. -/
theorem two_mul_pow_mul_ordinaryHypergeometric_inv_sq {𝕂 : Type*} [RCLike 𝕂]
    (n : ℕ) (c : {c : 𝕂 // (ascPochhammer 𝕂 (n / 2)).eval c ≠ 0}) (x : 𝕂ˣ) :
    (2 * x.val) ^ n * ordinaryHypergeometricOn (GaussParameters.quadratic n c.val c.property)
      (.ofTerminating _ (n / 2) (GaussParameters.quadratic_has_termination n _ _) (x.val ^ 2)⁻¹) =
      ∑ k : Fin (n / 2 + 1),
        (n.factorial : 𝕂) / (k.val.factorial * (n - 2 * k.val).factorial) *
          ((ascPochhammer 𝕂 k.val).eval c.val)⁻¹ * (2 * x.val) ^ (n - 2 * k.val) := by
  rw [ordinaryHypergeometricOn_terminating]
  rw [Fin.sum_univ_eq_sum_range (fun k : ℕ ↦
    (n.factorial : 𝕂) / (k.factorial * (n - 2 * k).factorial) *
      ((ascPochhammer 𝕂 k).eval c.val)⁻¹ * (2 * x.val) ^ (n - 2 * k)) (n / 2 + 1)]
  have hd (k : ℕ) : 4 ^ k * ((ascPochhammer 𝕂 k).eval (-(n : 𝕂) / 2) *
      (ascPochhammer 𝕂 k).eval ((1 - (n : 𝕂)) / 2)) = (n.descFactorial (2 * k) : 𝕂) := by
    rw [show ((1 : 𝕂) - n) / 2 = -(n : 𝕂) / 2 + 1 / 2 by ring,
      four_pow_mul_ascPochhammer_eval_mul_eval_add_half,
      show 2 * (-(n : 𝕂) / 2) = -(n : 𝕂) by ring, ascPochhammer_eval_neg_eq_descPochhammer,
      descPochhammer_eval_eq_descFactorial, pow_mul]
    norm_num
  have h4 (k : ℕ) : (4 : 𝕂) ^ k ≠ 0 := pow_ne_zero _ (by norm_num)
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun k hk ↦ ?_
  have hck := GaussParameters.pochhammer_ne_zero_of_le c.val c.property
    (Nat.le_of_lt_succ (Finset.mem_range.mp hk))
  rw [ordinaryHypergeometricCoefficientOn_eq_div _ k hck]
  simp only [GaussParameters.quadratic, GaussParameters.ofTerminating]
  have hk : 2 * k ≤ n := by
    have := Finset.mem_range.mp hk
    omega
  have hf : ((n - 2 * k).factorial : 𝕂) * n.descFactorial (2 * k) = n.factorial := by
    exact_mod_cast Nat.factorial_mul_descFactorial hk
  have hpow : (2 * x.val) ^ n = (2 * x.val) ^ (n - 2 * k) * (4 ^ k * (x.val ^ 2) ^ k) := by
    conv_lhs => rw [← Nat.sub_add_cancel hk]
    rw [pow_add, pow_mul]
    ring
  have hkf : (k.factorial : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero k)
  have hnf : ((n - 2 * k).factorial : 𝕂) ≠ 0 :=
    Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
  have hx2 : (x.val ^ 2) ^ k ≠ 0 := pow_ne_zero _ (pow_ne_zero _ (Units.ne_zero x))
  rw [hpow, ← hf, ← hd k, inv_pow]
  field_simp

3.3.2 Gegenbauer orthogonality and expansions

The weight is \((1-x^2)^{\lambda -1/2}\) on \((-1,1)\). Orthogonal expansions require \(\lambda {\gt}-1/2\) and \(\lambda \ne 0\); the measure itself is still meaningful at zero.

Definition 3.3.20 Gegenbauer measure

✓ 🙂 human-reviewed

#

For real \(\lambda \), let \(w_\lambda =w_{\lambda -1/2,\lambda -1/2}:(-1,1)\to \mathbb {R}_{\ge 0}\) be the Jacobi weight of Definition 3.2.9, and let \(\mu _\lambda =\mu _{w_\lambda }\) be the measure of Definition 1.1.2.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

def Polynomial.gegenbauerWeight (lam : ℝ) : C(↑(Set.Ioo (-1) 1), NNReal)

Lean definition

/-- The ultraspherical weight on its classical open domain (DLMF Table 18.3.1). -/
noncomputable def gegenbauerWeight (lam : ℝ) : C(Ioo (-1 : ℝ) 1, ℝ≥0) :=
  jacobiWeight (lam - 1 / 2) (lam - 1 / 2)

1 related Lean declaration

def Polynomial.gegenbauerMeasure (lam : ℝ) : MeasureTheory.Measure ℝ

Lean definition

/-- The Gegenbauer measure, obtained from its domain-typed density. -/
noncomputable def gegenbauerMeasure (lam : ℝ) : Measure ℝ :=
  openIntervalWeightMeasure (-1) 1 (gegenbauerWeight lam)

Theorem 3.3.21 Gegenbauer density and integral characterisation

✓ 🙂 human-reviewed

#

For every \(x\in (-1,1)\), \(w_\lambda (x)=(1-x^2)^{\lambda -1/2}\). A real function \(f\) is \(\mu _\lambda \)-integrable if and only if \(w_\lambda f\) is integrable on the open interval. When these equivalent integrability conditions hold,

\[ \int f\, d\mu _\lambda =\int _{x\in (-1,1)}w_\lambda (x)f(x)\, dx. \]

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.gegenbauerWeight_apply (lam : ℝ) (x : ↑(Set.Ioo (-1) 1)) :
  ↑((Polynomial.gegenbauerWeight lam) x) = (1 - ↑x ^ 2) ^ (lam - 1 / 2)

Lean proof

/-- The density formula at an interior point has a strictly positive power base. -/
theorem gegenbauerWeight_apply (lam : ℝ) (x : Ioo (-1 : ℝ) 1) :
    (gegenbauerWeight lam x : ℝ) = (1 - (x : ℝ) ^ 2) ^ (lam - 1 / 2) := by
  change (jacobiWeight (lam - 1 / 2) (lam - 1 / 2) x : ℝ) = _
  rw [jacobiWeight_apply, ← Real.mul_rpow
    (by linarith [x.property.2] : 0 ≤ 1 - (x : ℝ))
    (by linarith [x.property.1] : 0 ≤ 1 + (x : ℝ))]
  congr 1
  ring

2 related Lean declarations

theorem Polynomial.integrable_gegenbauerMeasure_iff (lam : ℝ) (f : ℝ → ℝ) :
  MeasureTheory.Integrable f (Polynomial.gegenbauerMeasure lam) ↔
    MeasureTheory.Integrable (fun x => ↑((Polynomial.gegenbauerWeight lam) x) * f ↑x) MeasureTheory.volume

Lean proof

/-- Integrability is equivalent to integrability of the classical density product. -/
theorem integrable_gegenbauerMeasure_iff (lam : ℝ) (f : ℝ → ℝ) :
    Integrable f (gegenbauerMeasure lam) ↔
      Integrable (fun x : Ioo (-1 : ℝ) 1 ↦ (gegenbauerWeight lam x : ℝ) * f x) volume :=
  integrable_openIntervalWeightMeasure_iff _ _ _ _

theorem Polynomial.integral_gegenbauerMeasure (lam : ℝ) (f : MeasureTheory.IntegrableInput (Polynomial.gegenbauerMeasure lam)) :
  ∫ (x : ℝ), ↑f x ∂Polynomial.gegenbauerMeasure lam =
    ∫ (x : ↑(Set.Ioo (-1) 1)), ↑((Polynomial.gegenbauerWeight lam) x) * ↑f ↑x

Lean proof

/-- Integral transport for an input bundled with its integrability witness. -/
theorem integral_gegenbauerMeasure (lam : ℝ)
    (f : IntegrableInput (gegenbauerMeasure lam)) :
    ∫ x, f.val x ∂gegenbauerMeasure lam =
      ∫ x : Ioo (-1 : ℝ) 1, (gegenbauerWeight lam x : ℝ) * f.val x :=
  integral_openIntervalWeightMeasure _ _ _ _

Theorem 3.3.22 Gegenbauer orthogonality

✓ 🤖

#

For \(\lambda {\gt}-1/2\) and \(m\ne n\),

\[ \int C_m^{(\lambda )}C_n^{(\lambda )}\, d\mu _\lambda =0. \]

For \(\lambda \ne 0\) the sequence satisfies the general orthogonality predicate. The pairwise integral identity itself also holds at \(\lambda =0\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integral_mul_gegenbauer_eq_zero {lam : ℝ} (hlam : -(1 / 2) < lam) {m n : ℕ} (hmn : m ≠ n) :
  ∫ (x : ℝ),
      Polynomial.eval x (Polynomial.gegenbauer lam m) *
        Polynomial.eval x (Polynomial.gegenbauer lam n) ∂Polynomial.gegenbauerMeasure lam =
    0

Lean proof

/-- Pairwise Gegenbauer orthogonality, also valid at the degenerate parameter zero
(DLMF Table 18.3.1). -/
theorem integral_mul_gegenbauer_eq_zero {lam : ℝ} (hlam : -(1 / 2) < lam)
    {m n : ℕ} (hmn : m ≠ n) :
    ∫ x, (gegenbauer lam m).eval x * (gegenbauer lam n).eval x ∂gegenbauerMeasure lam = 0 := by
  rw [gegenbauerMeasure_eq_jacobiMeasure]
  simp_rw [gegenbauer_eq_jacobi_mul hlam, eval_mul, eval_C]
  simp_rw [mul_mul_mul_comm]
  rw [integral_const_mul, integral_mul_jacobi_eq_zero (by linarith) (by linarith) hmn, mul_zero]

1 related Lean declaration

theorem Polynomial.isOrthogonal_gegenbauerSequence {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) :
  (Polynomial.gegenbauerSequence hlam hzero).IsOrthogonal (Polynomial.gegenbauerMeasure lam)

Lean proof

/-- Gegenbauer polynomials satisfy the general orthogonality predicate (DLMF Table 18.3.1). -/
theorem isOrthogonal_gegenbauerSequence {lam : ℝ} (hlam : -(1 / 2) < lam)
    (hzero : lam ≠ 0) : (gegenbauerSequence hlam hzero).IsOrthogonal (gegenbauerMeasure lam) where
  integrable _ _ := (hasFiniteMoments_gegenbauerMeasure hlam).integrable_mul _ _
  orthogonal _ _ hmn := integral_mul_gegenbauer_eq_zero hlam hmn

Theorem 3.3.23 Exact Gegenbauer squared norms

✓ 🤖

#

For \(\lambda {\gt}-1/2\), set \(h_n=\int (C_n^{(\lambda )})^2\, d\mu _\lambda \). Then

\[ h_0=\frac{\sqrt\pi \, \Gamma (\lambda +1/2)}{\Gamma (\lambda +1)}. \]

For \(n\ge 1\) and \(\lambda \ne 0\),

\[ h_n=\frac{2^{1-2\lambda }\pi \, \Gamma (n+2\lambda )}{(n+\lambda )\Gamma (\lambda )^2n!}. \]

The separate degree-zero formula also covers \(\lambda =0\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integral_sq_gegenbauer_zero {lam : ℝ} (hlam : -(1 / 2) < lam) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.gegenbauer lam 0) ^ 2 ∂Polynomial.gegenbauerMeasure lam =
    √Real.pi * Real.GammaOn (Real.GammaPoint.ofPos (lam + 1 / 2) ⋯) / Real.GammaOn (Real.GammaPoint.ofPos (lam + 1) ⋯)

Lean proof

/-- The classical Gamma formula; every displayed Gamma value excludes its poles. -/
theorem integral_sq_gegenbauer_zero {lam : ℝ} (hlam : -(1 / 2) < lam) :
    ∫ x, (gegenbauer lam 0).eval x ^ 2 ∂gegenbauerMeasure lam =
      √π * GammaOn (GammaPoint.ofPos (lam + 1 / 2) (by linarith)) / GammaOn (GammaPoint.ofPos (lam + 1) (by linarith)) :=
  integral_sq_gegenbauer_zero_gamma_formula hlam

1 related Lean declaration

theorem Polynomial.integral_sq_gegenbauer_succ {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.gegenbauer lam (n + 1)) ^ 2 ∂Polynomial.gegenbauerMeasure lam =
    2 ^ (1 - 2 * lam) * Real.pi * Real.GammaOn (Real.GammaPoint.ofPos (↑n + 1 + 2 * lam) ⋯) /
      ((↑n + 1 + lam) * Real.GammaOn ⟨lam, ⋯⟩ ^ 2 * ↑(n + 1).factorial)

Lean proof

/-- The classical Gamma formula; every displayed Gamma value excludes its poles. -/
theorem integral_sq_gegenbauer_succ {lam : ℝ} (hlam : -(1 / 2) < lam)
    (hzero : lam ≠ 0) (n : ℕ) :
    ∫ x, (gegenbauer lam (n + 1)).eval x ^ 2 ∂gegenbauerMeasure lam =
      (2 : ℝ) ^ (1 - 2 * lam) * π * GammaOn (GammaPoint.ofPos (n + 1 + 2 * lam) (by have _hn : (0 : ℝ) ≤ n := Nat.cast_nonneg n; linarith)) /
        (((n : ℝ) + 1 + lam) * GammaOn ⟨lam, by
          intro m he
          cases m with
          | zero => exact hzero (by simpa using he)
          | succ m =>
            have _hm := Nat.cast_nonneg (α := ℝ) m
            push_cast at he
            linarith⟩ ^ 2 * (n + 1).factorial) :=
  integral_sq_gegenbauer_succ_gamma_formula hlam hzero n

Definition 3.3.24 Gegenbauer coefficients

✓ 🤖

#

For \(f\in \mathcal A_{\mu _\lambda ,C_n^{(\lambda )}}^{\mathbb {R}}\), define \(a_n(f)=h_n^{-1}\int fC_n^{(\lambda )}\, d\mu _\lambda \), where \(h_n=\int (C_n^{(\lambda )})^2\, d\mu _\lambda \).

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

def Polynomial.gegenbauerCoefficient (lam : ℝ) {n : ℕ}
  (f : Polynomial.IntegralCoefficientInput ℝ (Polynomial.gegenbauerMeasure lam) (Polynomial.gegenbauer lam n)) : ℝ

Lean definition

/-- Gegenbauer integral coefficients on their full classical domain (DLMF 18.2(viii)). -/
@[expose] noncomputable def gegenbauerCoefficient (lam : ℝ) {n : ℕ}
    (f : IntegralCoefficientInput ℝ (gegenbauerMeasure lam) (gegenbauer lam n)) : ℝ :=
  (∫ x, (gegenbauer lam n).eval x ^ 2 ∂gegenbauerMeasure lam)⁻¹ *
    ∫ x, f.val x * (gegenbauer lam n).eval x ∂gegenbauerMeasure lam

1 related Lean declaration

def Polynomial.IntegralCoefficientInput.ofGegenbauerL2.{u_1} {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0)
  {𝕂 : Type u_1} [RCLike 𝕂] (f : ↥(MeasureTheory.Lp 𝕂 2 (Polynomial.gegenbauerMeasure lam))) (n : ℕ) :
  Polynomial.IntegralCoefficientInput 𝕂 (Polynomial.gegenbauerMeasure lam) (Polynomial.gegenbauer lam n)

Lean definition

/-- L2 data in the classical Gegenbauer range supply every coefficient input
(DLMF 18.2(viii)). -/
@[expose] noncomputable def IntegralCoefficientInput.ofGegenbauerL2 {𝕂 : Type*} [RCLike 𝕂]
    (f : Lp 𝕂 2 (gegenbauerMeasure lam)) (n : ℕ) :
    IntegralCoefficientInput 𝕂 (gegenbauerMeasure lam) (gegenbauer lam n) :=
  IntegralCoefficientInput.ofL2 (hasFiniteMoments_gegenbauerMeasure hlam) (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam)
    (gegenbauer lam n) (by simpa only [gegenbauerSequence_apply] using (gegenbauerSequence hlam hzero).ne_zero n) f

Theorem 3.3.25 Gegenbauer coefficient characterisation

✓ 🤖

#

For \(f\in \mathcal A_{\mu _\lambda ,C_n^{(\lambda )}}^{\mathbb {R}}\), \(a_n(f)=h_n^{-1}\int fC_n^{(\lambda )}\, d\mu _\lambda \), with an integrable numerator and finite positive \(h_n\). Under \(\lambda {\gt}-1/2\), \(\lambda \ne 0\), every \(L^2(\mu _\lambda )\) function belongs to this coefficient domain at every index, in the original polynomial normalization.

Lean Formalisation

theorem Polynomial.gegenbauerCoefficient_apply (lam : ℝ) {n : ℕ}
  (f : Polynomial.IntegralCoefficientInput ℝ (Polynomial.gegenbauerMeasure lam) (Polynomial.gegenbauer lam n)) :
  Polynomial.gegenbauerCoefficient lam f =
    (∫ (x : ℝ), Polynomial.eval x (Polynomial.gegenbauer lam n) ^ 2 ∂Polynomial.gegenbauerMeasure lam)⁻¹ *
      ∫ (x : ℝ), f.val x * Polynomial.eval x (Polynomial.gegenbauer lam n) ∂Polynomial.gegenbauerMeasure lam

Lean proof

/-- The classical weighted formula includes its integrability and positive normalization. -/
theorem gegenbauerCoefficient_apply (lam : ℝ) {n : ℕ}
    (f : IntegralCoefficientInput ℝ (gegenbauerMeasure lam) (gegenbauer lam n)) :
    gegenbauerCoefficient lam f =
      (∫ x, (gegenbauer lam n).eval x ^ 2 ∂gegenbauerMeasure lam)⁻¹ *
        ∫ x, f.val x * (gegenbauer lam n).eval x ∂gegenbauerMeasure lam := rfl

Normalization means dividing \(C_n^{(\lambda )}\) by \(\sqrt{h_n}\); \(J_\mu \) denotes its weighted \(L^2\) class.

Theorem 3.3.26 Gegenbauer completeness

✓ 🤖

#

For \(\lambda {\gt}-1/2\), \(\lambda \ne 0\), the normalised Gegenbauer polynomials form a Hilbert basis of real \(L^2(\mu _\lambda )\).

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

theorem Polynomial.polynomialToL2_gegenbauer_denseRange {lam : ℝ} (hlam : -(1 / 2) < lam) :
  DenseRange ⇑(Polynomial.polynomialToL2 ⋯)

Lean proof

/-- Gegenbauer polynomial classes are dense in weighted L² (DLMF 18.2(viii)). -/
theorem polynomialToL2_gegenbauer_denseRange :
    DenseRange (polynomialToL2 (hasFiniteMoments_gegenbauerMeasure hlam)) :=
  polynomialToL2_denseRange (hasFiniteMoments_gegenbauerMeasure hlam) (-1) 1
    ((ae_mem_Ioo_gegenbauerMeasure lam).mono (fun _ hx ↦ Set.Ioo_subset_Icc_self hx))

3 related Lean declarations

theorem Polynomial.orthonormal_normalizedGegenbauer {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) :
  Orthonormal ℝ (Polynomial.normalizedGegenbauer hlam hzero)

Lean proof

/-- The normalised Gegenbauer family is orthonormal (DLMF 18.2(viii)). -/
theorem orthonormal_normalizedGegenbauer : Orthonormal ℝ (normalizedGegenbauer hlam hzero) :=
  (isOrthogonal_gegenbauerSequence hlam hzero).orthonormal_normalizedToL2
    (hasFiniteMoments_gegenbauerMeasure hlam) (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam)

def Polynomial.hilbertBasisGegenbauer {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) :
  HilbertBasis ℕ ℝ ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))

Lean definition

/-- The Gegenbauer Hilbert basis (DLMF 18.2(viii)). -/
noncomputable def hilbertBasisGegenbauer : HilbertBasis ℕ ℝ (Lp ℝ 2 (gegenbauerMeasure lam)) :=
  (isOrthogonal_gegenbauerSequence hlam hzero).hilbertBasis
    (hasFiniteMoments_gegenbauerMeasure hlam)
    (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam) (polynomialToL2_gegenbauer_denseRange hlam)

theorem Polynomial.hilbertBasisGegenbauer_apply {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) :
  (Polynomial.hilbertBasisGegenbauer hlam hzero) n = Polynomial.normalizedGegenbauer hlam hzero n

Lean proof

/-- The Hilbert basis vectors are the normalised Gegenbauer classes (DLMF 18.2(viii)). -/
@[simp] theorem hilbertBasisGegenbauer_apply (n : ℕ) :
    hilbertBasisGegenbauer hlam hzero n = normalizedGegenbauer hlam hzero n :=
  (isOrthogonal_gegenbauerSequence hlam hzero).hilbertBasis_apply
    (hasFiniteMoments_gegenbauerMeasure hlam)
    (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam)
    (polynomialToL2_gegenbauer_denseRange hlam) n

Theorem 3.3.27 Gegenbauer L2 expansions

✓ 🤖

#

For \(\lambda {\gt}-1/2\), \(\lambda \ne 0\), and every \(f\in L^2(\mu _\lambda )\), the series \(\sum _{n\ge 0}a_n(f)J_{\mu _\lambda }C_n^{(\lambda )}\) sums to \(f\). Its natural-order partial sums converge in \(L^2\).

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

theorem Polynomial.hasSum_gegenbauerCoefficient_polynomialToL2 {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0)
  (f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
  HasSum
    (fun n =>
      Polynomial.gegenbauerCoefficient lam (Polynomial.IntegralCoefficientInput.ofGegenbauerL2 hlam hzero f n) •
        (Polynomial.polynomialToL2 ⋯) (Polynomial.gegenbauer lam n))
    f

Lean proof

/-- Every weighted L² function is the sum of its Gegenbauer series in L² (DLMF 18.2(viii)). -/
theorem hasSum_gegenbauerCoefficient_polynomialToL2 (f : Lp ℝ 2 (gegenbauerMeasure lam)) :
    HasSum (fun n ↦ (gegenbauerCoefficient lam (IntegralCoefficientInput.ofGegenbauerL2 hlam hzero f n)) •
      polynomialToL2 (hasFiniteMoments_gegenbauerMeasure hlam) (gegenbauer lam n)) f := by
  simpa only [Sequence.integralCoefficient, squaredNorm_gegenbauerSequence, gegenbauerSequence_apply,
    gegenbauerCoefficient, IntegralCoefficientInput.ofGegenbauerL2, IntegralCoefficientInput.ofL2] using
    (isOrthogonal_gegenbauerSequence hlam hzero).hasSum_integralCoefficient
      (hasFiniteMoments_gegenbauerMeasure hlam) (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam)
      (polynomialToL2_gegenbauer_denseRange hlam) f

1 related Lean declaration

theorem Polynomial.tendsto_sum_gegenbauerCoefficient_polynomialToL2 {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0)
  (f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
  Filter.Tendsto
    (fun N =>
      ∑ n ∈ Finset.range N,
        Polynomial.gegenbauerCoefficient lam (Polynomial.IntegralCoefficientInput.ofGegenbauerL2 hlam hzero f n) •
          (Polynomial.polynomialToL2 ⋯) (Polynomial.gegenbauer lam n))
    Filter.atTop (nhds f)

Lean proof

/-- Natural-order Gegenbauer partial sums converge in L² (DLMF 18.2(viii)). -/
theorem tendsto_sum_gegenbauerCoefficient_polynomialToL2 (f : Lp ℝ 2 (gegenbauerMeasure lam)) :
    Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.range N, (gegenbauerCoefficient lam (IntegralCoefficientInput.ofGegenbauerL2 hlam hzero f n)) •
      polynomialToL2 (hasFiniteMoments_gegenbauerMeasure hlam) (gegenbauer lam n)) atTop (nhds f) :=
  (hasSum_gegenbauerCoefficient_polynomialToL2 hlam hzero f).tendsto_sum_nat

Theorem 3.3.28 Gegenbauer root location

✓ 🤖

#

For \(\lambda {\gt}-1/2\), \(\lambda \ne 0\), \(C_n^{(\lambda )}\) is orthogonal to every polynomial of degree below \(n\), and every real root lies in \((-1,1)\).

Reference: [DLMF, 18.2(i), (vi)].

Lean Formalisation

theorem Polynomial.integral_mul_gegenbauer_eq_zero_of_degree_lt {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0)
  {p : Polynomial ℝ} {n : ℕ} (hp : p.degree < ↑n) :
  ∫ (x : ℝ), Polynomial.eval x p * Polynomial.eval x (Polynomial.gegenbauer lam n) ∂Polynomial.gegenbauerMeasure lam = 0

Lean proof

/-- Orthogonality to every lower-degree polynomial (DLMF 18.2(i)). -/
theorem integral_mul_gegenbauer_eq_zero_of_degree_lt {p : ℝ[X]} {n : ℕ} (hp : p.degree < n) :
    ∫ x, p.eval x * (gegenbauer lam n).eval x ∂gegenbauerMeasure lam = 0 :=
  (isOrthogonal_gegenbauerSequence hlam hzero).integralInner_eq_zero_of_degree_lt
    (hasFiniteMoments_gegenbauerMeasure hlam) hp

1 related Lean declaration

theorem Polynomial.root_gegenbauer_mem_Ioo {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) {n : ℕ} {x : ℝ}
  (hx : Polynomial.eval x (Polynomial.gegenbauer lam n) = 0) : x ∈ Set.Ioo (-1) 1

Lean proof

/-- Every Gegenbauer root lies strictly inside the interval (DLMF 18.2(vi)). -/
theorem root_gegenbauer_mem_Ioo {n : ℕ} {x : ℝ}
    (hx : (gegenbauer lam n).eval x = 0) : x ∈ Ioo (-1) 1 := by
  rw [gegenbauer_eq_jacobi_mul hlam, eval_mul, eval_C] at hx
  exact root_jacobi_mem_Ioo (by linarith) (by linarith)
    ((mul_eq_zero.mp hx).resolve_left (gegenbauer_jacobi_factor_ne_zero hlam hzero n))

Theorem 3.3.29 Gegenbauer strict interlacing

✓ 🤖

#

For \(\lambda {\gt}-1/2\), \(\lambda \ne 0\), consecutive Gegenbauer polynomials have no common zero and mutually separate each other’s real zeros. For \(n\ge 1\), \(C_{n+1}^{(\lambda )}\) has roots \(a{\lt}b\) with every root of \(C_n^{(\lambda )}\) strictly between them.

Reference: [DLMF, 18.2(vi)].

Lean Formalisation

theorem Polynomial.not_eval_gegenbauer_eq_zero_and_succ {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) (x : ℝ) :
  ¬(Polynomial.eval x (Polynomial.gegenbauer lam n) = 0 ∧ Polynomial.eval x (Polynomial.gegenbauer lam (n + 1)) = 0)

Lean proof

/-- Consecutive members have no common root (DLMF 18.2(vi)). -/
theorem not_eval_gegenbauer_eq_zero_and_succ (n : ℕ) (x : ℝ) :
    ¬ ((gegenbauer lam n).eval x = 0 ∧ (gegenbauer lam (n + 1)).eval x = 0) :=
  (isOrthogonal_gegenbauerSequence hlam hzero).not_eval_eq_zero_and_succ
    (hasFiniteMoments_gegenbauerMeasure hlam)
    (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam) n x

3 related Lean declarations

theorem Polynomial.exists_root_gegenbauer_succ_between {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) {a b : ℝ}
  (hab : a < b) (ha : Polynomial.eval a (Polynomial.gegenbauer lam n) = 0)
  (hb : Polynomial.eval b (Polynomial.gegenbauer lam n) = 0) :
  ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.gegenbauer lam (n + 1)) = 0

Lean proof

/-- Between degree-n roots lies a degree-(n+1) root (DLMF 18.2(vi)). -/
theorem exists_root_gegenbauer_succ_between (n : ℕ) {a b : ℝ} (hab : a < b)
    (ha : (gegenbauer lam n).eval a = 0) (hb : (gegenbauer lam n).eval b = 0) :
    ∃ c ∈ Ioo a b, (gegenbauer lam (n + 1)).eval c = 0 :=
  (isOrthogonal_gegenbauerSequence hlam hzero).exists_root_succ_between
    (hasFiniteMoments_gegenbauerMeasure hlam)
    (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam) n hab ha hb

theorem Polynomial.exists_root_gegenbauer_between_succ {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) {a b : ℝ}
  (hab : a < b) (ha : Polynomial.eval a (Polynomial.gegenbauer lam (n + 1)) = 0)
  (hb : Polynomial.eval b (Polynomial.gegenbauer lam (n + 1)) = 0) :
  ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.gegenbauer lam n) = 0

Lean proof

/-- Between degree-(n+1) roots lies a degree-n root (DLMF 18.2(vi)). -/
theorem exists_root_gegenbauer_between_succ (n : ℕ) {a b : ℝ} (hab : a < b)
    (ha : (gegenbauer lam (n + 1)).eval a = 0) (hb : (gegenbauer lam (n + 1)).eval b = 0) :
    ∃ c ∈ Ioo a b, (gegenbauer lam n).eval c = 0 :=
  (isOrthogonal_gegenbauerSequence hlam hzero).exists_root_between_succ
    (hasFiniteMoments_gegenbauerMeasure hlam)
    (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam) n hab ha hb

theorem Polynomial.exists_outer_roots_gegenbauer {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) {n : ℕ} (hn : 1 ≤ n) :
  ∃ a b,
    a < b ∧
      Polynomial.eval a (Polynomial.gegenbauer lam (n + 1)) = 0 ∧
        Polynomial.eval b (Polynomial.gegenbauer lam (n + 1)) = 0 ∧
          ∀ (x : ℝ), Polynomial.eval x (Polynomial.gegenbauer lam n) = 0 → a < x ∧ x < b

Lean proof

/-- The higher-degree member has both outermost roots (DLMF 18.2(vi)). -/
theorem exists_outer_roots_gegenbauer {n : ℕ} (hn : 1 ≤ n) :
    ∃ a b : ℝ, a < b ∧ (gegenbauer lam (n + 1)).eval a = 0 ∧
      (gegenbauer lam (n + 1)).eval b = 0 ∧
      ∀ x : ℝ, (gegenbauer lam n).eval x = 0 → a < x ∧ x < b :=
  (isOrthogonal_gegenbauerSequence hlam hzero).exists_outer_roots
    (hasFiniteMoments_gegenbauerMeasure hlam)
    (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam) hn

Measure bridges, norm transfer and normalization

Theorem 3.3.30 Gegenbauer coefficients as general coefficients

✓ 🤖

#

For \(\lambda {\gt}-1/2\), \(\lambda \ne 0\), the integral coefficients of the Gegenbauer sequence for \(\mu _\lambda \) (Definition 3.1.38) are the Gegenbauer coefficients \(a_n(f)\), for \(f\in \mathcal A_{\mu _\lambda ,C_n^{(\lambda )}}^{\mathbb {R}}\).

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

theorem Polynomial.integralCoefficient_gegenbauerSequence {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) {n : ℕ}
  (f : Polynomial.IntegralCoefficientInput ℝ (Polynomial.gegenbauerMeasure lam) (Polynomial.gegenbauer lam n)) :
  (Polynomial.gegenbauerSequence hlam hzero).integralCoefficient (Polynomial.gegenbauerMeasure lam) f =
    Polynomial.gegenbauerCoefficient lam f

Lean proof

/-- The generic integral coefficients are the Gegenbauer coefficients on the
classical input domain (DLMF 18.2(viii)). -/
theorem integralCoefficient_gegenbauerSequence {n : ℕ}
    (f : IntegralCoefficientInput ℝ (gegenbauerMeasure lam) (gegenbauer lam n)) :
    (gegenbauerSequence hlam hzero).integralCoefficient (gegenbauerMeasure lam) f =
      gegenbauerCoefficient lam f := by
  simp only [Sequence.integralCoefficient, squaredNorm_gegenbauerSequence,
    gegenbauerSequence_apply, gegenbauerCoefficient]

Theorem 3.3.31 Gegenbauer–Jacobi measure bridge

✓ 🙂 human-reviewed

#

For every real \(\lambda \), the Gegenbauer weight equals \(w_{\lambda -1/2,\lambda -1/2}\) on \((-1,1)\), and \(\mu _\lambda =\mu _{\lambda -1/2,\lambda -1/2}\). The measure assigns zero mass to \(\mathbb {R}\setminus (-1,1)\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.gegenbauerWeight_eq_jacobiWeight (lam : ℝ) :
  Polynomial.gegenbauerWeight lam = Polynomial.jacobiWeight (lam - 1 / 2) (lam - 1 / 2)

Lean proof

/-- The symmetric Jacobi identity is an equality of domain-typed weights. -/
theorem gegenbauerWeight_eq_jacobiWeight (lam : ℝ) :
    gegenbauerWeight lam = jacobiWeight (lam - 1 / 2) (lam - 1 / 2) := rfl

2 related Lean declarations

theorem Polynomial.gegenbauerMeasure_eq_jacobiMeasure (lam : ℝ) :
  Polynomial.gegenbauerMeasure lam = Polynomial.jacobiMeasure (lam - 1 / 2) (lam - 1 / 2)

Lean proof

/-- Equality with the symmetric Jacobi measure (DLMF Table 18.3.1). -/
theorem gegenbauerMeasure_eq_jacobiMeasure (lam : ℝ) :
    gegenbauerMeasure lam = jacobiMeasure (lam - 1 / 2) (lam - 1 / 2) := rfl

theorem Polynomial.ae_mem_Ioo_gegenbauerMeasure (lam : ℝ) : ∀ᵐ (x : ℝ) ∂Polynomial.gegenbauerMeasure lam, x ∈ Set.Ioo (-1) 1

Lean proof

/-- The measure is concentrated on the open interval (DLMF Table 18.3.1). -/
theorem ae_mem_Ioo_gegenbauerMeasure (lam : ℝ) :
    ∀ᵐ x ∂gegenbauerMeasure lam, x ∈ Ioo (-1) 1 := by
  rw [gegenbauerMeasure_eq_jacobiMeasure]
  exact ae_mem_Ioo_jacobiMeasure _ _

Theorem 3.3.32 Gegenbauer moments and positivity

✓ 🤖

#

For \(\lambda {\gt}-1/2\), the weight is integrable, every real-valued function continuous on \([-1,1]\) is \(\mu _\lambda \)-integrable, all polynomial moments are finite, and \(\int p^2\, d\mu _\lambda {\gt}0\) for every nonzero polynomial \(p\). The measure has finite total mass. These assertions include \(\lambda =0\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integrable_gegenbauerWeight {lam : ℝ} (hlam : -(1 / 2) < lam) :
  MeasureTheory.Integrable (fun x => ↑((Polynomial.gegenbauerWeight lam) x)) MeasureTheory.volume

Lean proof

/-- Integrability of the open-domain ultraspherical density in its full range. -/
theorem integrable_gegenbauerWeight {lam : ℝ} (hlam : -(1 / 2) < lam) :
    Integrable (fun x : Ioo (-1 : ℝ) 1 ↦ (gegenbauerWeight lam x : ℝ)) volume :=
  integrable_jacobiWeight (by linarith) (by linarith)

4 related Lean declarations

theorem Polynomial.integrable_gegenbauerMeasure {lam : ℝ} (hlam : -(1 / 2) < lam) {f : ℝ → ℝ}
  (hf : ContinuousOn f (Set.Icc (-1) 1)) : MeasureTheory.Integrable f (Polynomial.gegenbauerMeasure lam)

Lean proof

/-- Continuous functions on the closed interval are integrable (DLMF Table 18.3.1). -/
theorem integrable_gegenbauerMeasure {lam : ℝ} (hlam : -(1 / 2) < lam)
    {f : ℝ → ℝ} (hf : ContinuousOn f (Icc (-1) 1)) :
    Integrable f (gegenbauerMeasure lam) := by
  rw [gegenbauerMeasure_eq_jacobiMeasure]
  exact integrable_jacobiMeasure (by linarith) (by linarith) hf

theorem Polynomial.hasFiniteMoments_gegenbauerMeasure {lam : ℝ} (hlam : -(1 / 2) < lam) :
  Polynomial.HasFiniteMoments (Polynomial.gegenbauerMeasure lam)

Lean proof

/-- All polynomial moments are finite (DLMF Table 18.3.1). -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasFiniteMoments_gegenbauerMeasure {lam : ℝ} (hlam : -(1 / 2) < lam) :
    HasFiniteMoments (gegenbauerMeasure lam) := by
  rw [gegenbauerMeasure_eq_jacobiMeasure]
  exact hasFiniteMoments_jacobiMeasure (by linarith) (by linarith)

theorem Polynomial.isFiniteMeasure_gegenbauerMeasure {lam : ℝ} (hlam : -(1 / 2) < lam) :
  MeasureTheory.IsFiniteMeasure (Polynomial.gegenbauerMeasure lam)

Lean proof

/-- The Gegenbauer measure is finite (DLMF Table 18.3.1). -/
theorem isFiniteMeasure_gegenbauerMeasure {lam : ℝ} (hlam : -(1 / 2) < lam) :
    IsFiniteMeasure (gegenbauerMeasure lam) :=
  (hasFiniteMoments_gegenbauerMeasure hlam).isFiniteMeasure

theorem Polynomial.hasPositiveDefiniteIntegral_gegenbauerMeasure {lam : ℝ} (hlam : -(1 / 2) < lam) :
  Polynomial.HasPositiveDefiniteIntegral (Polynomial.gegenbauerMeasure lam)

Lean proof

/-- The polynomial integral pairing is positive definite (DLMF Table 18.3.1). -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasPositiveDefiniteIntegral_gegenbauerMeasure {lam : ℝ}
    (hlam : -(1 / 2) < lam) : HasPositiveDefiniteIntegral (gegenbauerMeasure lam) := by
  rw [gegenbauerMeasure_eq_jacobiMeasure]
  exact hasPositiveDefiniteIntegral_jacobiMeasure (by linarith) (by linarith)

Theorem 3.3.33 Divided Gegenbauer–Jacobi bridge

✓ 🤖

#

For \(\lambda {\gt}-1/2\), write \(c_n=(2\lambda )_n/(\lambda +1/2)_n\). Then

\[ C_n^{(\lambda )}=c_nP_n^{(\lambda -1/2,\lambda -1/2)}. \]

If additionally \(\lambda \ne 0\), every \(c_n\) is nonzero, including when \(-1/2{\lt}\lambda {\lt}0\).

Reference: [DLMF, 18.7.1].

Lean Formalisation

theorem Polynomial.gegenbauer_eq_jacobi_mul {lam : ℝ} (hlam : -(1 / 2) < lam) (n : ℕ) :
  Polynomial.gegenbauer lam n =
    Polynomial.C (Polynomial.eval (2 * lam) (ascPochhammer ℝ n) / Polynomial.eval (lam + 1 / 2) (ascPochhammer ℝ n)) *
      Polynomial.jacobi (lam - 1 / 2) (lam - 1 / 2) n

Lean proof

/-- The divided bridge in the orthogonality range (DLMF 18.7.1).
It includes parameter zero, where positive-degree Gegenbauer polynomials vanish. -/
theorem gegenbauer_eq_jacobi_mul {lam : ℝ} (hlam : -(1 / 2) < lam) (n : ℕ) :
    gegenbauer lam n =
      C ((ascPochhammer ℝ n).eval (2 * lam) /
        (ascPochhammer ℝ n).eval (lam + 1 / 2)) *
          jacobi (lam - 1 / 2) (lam - 1 / 2) n := by
  have hd : (ascPochhammer ℝ n).eval (lam + 1 / 2) ≠ 0 :=
    (ascPochhammer_pos n _ (by linarith)).ne'
  have h := gegenbauer_jacobi lam n
  norm_num only [map_div₀, map_one, map_ofNat] at h
  apply mul_left_cancel₀ (C_ne_zero.mpr hd)
  rw [h, ← mul_assoc, ← C_mul, mul_div_cancel₀ _ hd]

1 related Lean declaration

theorem Polynomial.gegenbauer_jacobi_factor_ne_zero {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) :
  Polynomial.eval (2 * lam) (ascPochhammer ℝ n) / Polynomial.eval (lam + 1 / 2) (ascPochhammer ℝ n) ≠ 0

Lean proof

/-- The bridge factor is nonzero for nonzero admissible parameters (DLMF 18.7.1). -/
theorem gegenbauer_jacobi_factor_ne_zero {lam : ℝ} (hlam : -(1 / 2) < lam)
    (hzero : lam ≠ 0) (n : ℕ) :
    (ascPochhammer ℝ n).eval (2 * lam) /
      (ascPochhammer ℝ n).eval (lam + 1 / 2) ≠ 0 := by
  apply div_ne_zero _ (ascPochhammer_pos n _ (by linarith)).ne'
  induction n with
  | zero => simp
  | succ n ih =>
    rw [ascPochhammer_succ_eval]
    apply mul_ne_zero ih
    rcases n with _ | n
    · simpa using (mul_ne_zero (by norm_num : (2 : ℝ) ≠ 0) hzero)
    · have : 0 < 2 * lam + (n + 1 : ℕ) := by
        push_cast
        linarith [Nat.cast_nonneg (α := ℝ) n]
      exact this.ne'

Theorem 3.3.34 Gegenbauer polynomial sequence

✓ 🤖

#

For \(\lambda {\gt}-1/2\), \(\lambda \ne 0\), \(C_n^{(\lambda )}\) has exact degree \(n\) and these polynomials define a degree-indexed sequence.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.degree_gegenbauer_of_neg_half_lt {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) :
  (Polynomial.gegenbauer lam n).degree = ↑n

Lean proof

/-- Exact degree throughout the nondegenerate orthogonality range (DLMF Table 18.3.1). -/
theorem degree_gegenbauer_of_neg_half_lt {lam : ℝ} (hlam : -(1 / 2) < lam)
    (hzero : lam ≠ 0) (n : ℕ) : (gegenbauer lam n).degree = n := by
  rw [gegenbauer_eq_jacobi_mul hlam, degree_C_mul (gegenbauer_jacobi_factor_ne_zero hlam hzero n)]
  exact degree_jacobi_of_neg_one_lt (by linarith) (by linarith) n

2 related Lean declarations

def Polynomial.gegenbauerSequence {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) : Polynomial.Sequence ℝ

Lean definition

/-- The Gegenbauer polynomial sequence (DLMF Table 18.3.1). -/
@[expose] noncomputable def gegenbauerSequence {lam : ℝ} (hlam : -(1 / 2) < lam)
    (hzero : lam ≠ 0) : Sequence ℝ where
  elems' := gegenbauer lam
  degree_eq' := degree_gegenbauer_of_neg_half_lt hlam hzero

theorem Polynomial.gegenbauerSequence_apply {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) :
  ↑(Polynomial.gegenbauerSequence hlam hzero) n = Polynomial.gegenbauer lam n

Lean proof

/-- The sequence uses the independent Gegenbauer definition (DLMF Table 18.3.1). -/
@[simp] theorem gegenbauerSequence_apply {lam : ℝ} (hlam : -(1 / 2) < lam)
    (hzero : lam ≠ 0) (n : ℕ) : gegenbauerSequence hlam hzero n = gegenbauer lam n := rfl

Theorem 3.3.35 Gegenbauer norm transfer

✓ 🤖

#

For \(\lambda {\gt}-1/2\), the squared norm of \(C_n^{(\lambda )}\) is \(c_n^2\) times the squared norm of \(P_n^{(\lambda -1/2,\lambda -1/2)}\), with \(c_n\) as in the divided bridge.

Reference: [DLMF, 18.7.1].

Lean Formalisation

theorem Polynomial.integral_sq_gegenbauer_eq_jacobi {lam : ℝ} (hlam : -(1 / 2) < lam) (n : ℕ) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.gegenbauer lam n) ^ 2 ∂Polynomial.gegenbauerMeasure lam =
    (Polynomial.eval (2 * lam) (ascPochhammer ℝ n) / Polynomial.eval (lam + 1 / 2) (ascPochhammer ℝ n)) ^ 2 *
      ∫ (x : ℝ),
        Polynomial.eval x (Polynomial.jacobi (lam - 1 / 2) (lam - 1 / 2) n) ^
          2 ∂Polynomial.jacobiMeasure (lam - 1 / 2) (lam - 1 / 2)

Lean proof

/-- Squared norms transfer with the square of the bridge factor (DLMF 18.7.1). -/
theorem integral_sq_gegenbauer_eq_jacobi {lam : ℝ} (hlam : -(1 / 2) < lam) (n : ℕ) :
    (∫ x, (gegenbauer lam n).eval x ^ 2 ∂gegenbauerMeasure lam) =
      ((ascPochhammer ℝ n).eval (2 * lam) /
        (ascPochhammer ℝ n).eval (lam + 1 / 2)) ^ 2 *
          ∫ x, (jacobi (lam - 1 / 2) (lam - 1 / 2) n).eval x ^ 2
            ∂jacobiMeasure (lam - 1 / 2) (lam - 1 / 2) := by
  rw [gegenbauerMeasure_eq_jacobiMeasure]
  simp_rw [gegenbauer_eq_jacobi_mul hlam, eval_mul, eval_C, mul_pow]
  exact integral_const_mul _ _

Theorem 3.3.36 Real simple Gegenbauer zeros

✓ 🤖

#

For \(\lambda {\gt}-1/2\), \(\lambda \ne 0\), \(C_n^{(\lambda )}\) splits over \(\mathbb {R}\), is separable, and has \(n\) roots counted with multiplicity, hence \(n\) distinct real zeros.

Reference: [DLMF, 18.2(vi)].

Lean Formalisation

theorem Polynomial.splits_gegenbauer {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) :
  (Polynomial.gegenbauer lam n).Splits

Lean proof

/-- Gegenbauer polynomials split over the reals (DLMF 18.2(vi)). -/
theorem splits_gegenbauer (n : ℕ) : (gegenbauer lam n).Splits :=
  (isOrthogonal_gegenbauerSequence hlam hzero).splits (hasFiniteMoments_gegenbauerMeasure hlam)
    (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam) n

2 related Lean declarations

theorem Polynomial.card_roots_gegenbauer {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) :
  (Polynomial.gegenbauer lam n).roots.card = n

Lean proof

/-- There are degree-many Gegenbauer roots (DLMF 18.2(vi)). -/
theorem card_roots_gegenbauer (n : ℕ) : (gegenbauer lam n).roots.card = n :=
  (isOrthogonal_gegenbauerSequence hlam hzero).card_roots (hasFiniteMoments_gegenbauerMeasure hlam)
    (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam) n

theorem Polynomial.separable_gegenbauer {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) :
  (Polynomial.gegenbauer lam n).Separable

Lean proof

/-- All Gegenbauer roots are simple (DLMF 18.2(vi)). -/
theorem separable_gegenbauer (n : ℕ) : (gegenbauer lam n).Separable :=
  (isOrthogonal_gegenbauerSequence hlam hzero).separable (hasFiniteMoments_gegenbauerMeasure hlam)
    (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam) n

Definition 3.3.37 Normalised Gegenbauer classes

✓ 🤖

#

For \(\lambda {\gt}-1/2\), \(\lambda \ne 0\), let \(e_n=h_n^{-1/2}J_{\mu _\lambda }C_n^{(\lambda )}\), using the positive square root of the squared norm.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

def Polynomial.normalizedGegenbauer {lam : ℝ} (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0) (n : ℕ) :
  ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))

Lean definition

/-- Normalised Gegenbauer classes (DLMF Table 18.3.1). -/
noncomputable def normalizedGegenbauer (n : ℕ) : Lp ℝ 2 (gegenbauerMeasure lam) :=
  (gegenbauerSequence hlam hzero).normalizedToL2 (hasFiniteMoments_gegenbauerMeasure hlam) ⟨n, Sequence.squaredNorm_pos (hasPositiveDefiniteIntegral_gegenbauerMeasure hlam) (gegenbauerSequence hlam hzero) n⟩

3.3.3 Legendre polynomials

Legendre polynomials are the Jacobi case \(\alpha =\beta =0\), normalized by \(P_n(1)=1\). Their orthogonality measure is ordinary Lebesgue measure on the interval.

Definition 3.3.38 Legendre polynomials

✓ 🙂 human-reviewed

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). Define (Rodrigues’ formula)

\[ P_n(X)=\frac{1}{2^n n!}\left(\frac{d}{dX}\right)^n(X^2-1)^n. \]

Reference: [DLMF, 18.5.5, Table 18.5.1 and Table 18.3.1].

Lean Formalisation

def Polynomial.legendre.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) : Polynomial R

Lean definition

/-- Legendre polynomials in the normalisation `Pₙ(1) = 1`, defined by
Rodrigues' formula (DLMF 18.5.5, Table 18.5.1 and Table 18.3.1). -/
noncomputable def legendre (n : ℕ) : R[X] :=
  C (algebraMap ℚ R (((2 : ℚ) ^ n * n.factorial)⁻¹)) *
    derivative^[n] ((X ^ 2 - 1) ^ n)

Theorem 3.3.39 Legendre–Jacobi bridge

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). Then \(P_n=P_n^{(0,0)}\).

Reference: [DLMF, 18.7.9].

Lean Formalisation

theorem Polynomial.legendre_eq_jacobi.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  Polynomial.legendre R n = Polynomial.jacobi 0 0 n

Lean proof

/-- The Rodrigues Legendre family equals the Jacobi family with both parameters
zero (DLMF Table 18.3.1). -/
theorem legendre_eq_jacobi (n : ℕ) : legendre R n = jacobi (0 : R) 0 n := by
  rw [legendre_eq_shiftedLegendre_comp]
  simp only [shiftedLegendre, jacobi, Polynomial.map_sum, Polynomial.map_mul,
    Polynomial.map_pow, Polynomial.map_neg, Polynomial.map_one, Polynomial.map_natCast,
    neg_comp, one_comp, natCast_comp, map_X, sum_comp, mul_comp, pow_comp, X_comp,
    map_mul, map_pow, map_neg, map_one, map_natCast, add_zero, zero_add]
  apply Finset.sum_congr rfl
  intro k hk
  have hkn : k ≤ n := by simpa using hk
  have hchoose : (n + k).choose k = (n + k).choose n := by
    simpa using (Nat.choose_symm (Nat.le_add_left k n)).symm
  rw [pochhammer_nat_succ, pochhammer_nat_succ, Nat.add_sub_of_le hkn,
    Nat.choose_symm hkn, hchoose]
  have hc : algebraMap ℚ R (((k.factorial : ℚ) * (n - k).factorial * 2 ^ k)⁻¹) *
      (k.factorial : R) * ((n - k).factorial : R) = algebraMap ℚ R ((1 / 2 : ℚ) ^ k) := by
    have h : (((k.factorial : ℚ) * (n - k).factorial * 2 ^ k)⁻¹) *
        k.factorial * (n - k).factorial = (1 / 2 : ℚ) ^ k := by
      rw [div_pow, one_pow]
      field_simp
    simpa only [map_mul, map_natCast] using congrArg (algebraMap ℚ R) h
  have hbase : (C (-1 : R) * (C (algebraMap ℚ R (1 / 2)) * (1 - X))) =
      C (algebraMap ℚ R (1 / 2)) * (X - 1) := by simp only [map_neg, map_one]; ring
  calc
    _ = C (n.choose k : R) * C ((n + k).choose n : R) *
        (C (-1 : R) * (C (algebraMap ℚ R (1 / 2)) * (1 - X))) ^ k := by
      simp only [mul_pow, map_neg, map_one, map_natCast]
      ring
    _ = C (n.choose k : R) * C ((n + k).choose n : R) *
        (C (algebraMap ℚ R (1 / 2)) * (X - 1)) ^ k := by rw [hbase]
    _ = C (algebraMap ℚ R (((k.factorial : ℚ) * (n - k).factorial * 2 ^ k)⁻¹) *
        (k.factorial : R) * ((n - k).factorial : R)) *
        C (n.choose k : R) * C ((n + k).choose n : R) * (X - 1) ^ k := by
      rw [hc]
      simp only [map_pow, mul_pow]
      ring
    _ = _ := by simp only [map_mul]; ring

Theorem 3.3.40 Legendre endpoint values

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). The Legendre polynomials satisfy \(P_0=1\), \(P_1=X\), \(P_n(1)=1\), and \(P_n(-1)=(-1)^n\).

Reference: [DLMF, Table 18.6.1].

Lean Formalisation

theorem Polynomial.legendre_zero.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] : Polynomial.legendre R 0 = 1

Lean proof

/-- The constant Legendre polynomial (DLMF Table 18.3.1). -/
@[simp] theorem legendre_zero : legendre R 0 = 1 := by
  rw [legendre_eq_jacobi, jacobi_zero]

3 related Lean declarations

theorem Polynomial.legendre_one.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] : Polynomial.legendre R 1 = Polynomial.X

Lean proof

/-- The first Legendre polynomial (DLMF Table 18.3.1). -/
@[simp] theorem legendre_one : legendre R 1 = X := by
  rw [legendre_eq_jacobi, jacobi_one]
  have hh : algebraMap ℚ R (1 / 2) * (2 : R) = 1 := by
    have h := congrArg (algebraMap ℚ R) (show (1 / 2 : ℚ) * 2 = 1 by norm_num)
    simpa only [map_mul, map_ofNat, map_one] using h
  simp only [zero_add, hh, C_1, one_mul]
  ring

theorem Polynomial.eval_legendre_one.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  Polynomial.eval 1 (Polynomial.legendre R n) = 1

Lean proof

/-- The endpoint normalisation of Legendre polynomials (DLMF Table 18.6.1). -/
@[simp] theorem eval_legendre_one (n : ℕ) : (legendre R n).eval 1 = 1 := by
  rw [legendre_eq_jacobi, eval_jacobi_one]
  simp only [zero_add, ascPochhammer_eval_one]
  have h := congrArg (algebraMap ℚ R)
    (inv_mul_cancel₀ (show (n.factorial : ℚ) ≠ 0 by positivity))
  simpa only [map_mul, map_natCast, map_one] using h

theorem Polynomial.eval_legendre_neg_one.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  Polynomial.eval (-1) (Polynomial.legendre R n) = (-1) ^ n

Lean proof

/-- The value at the left endpoint (DLMF Table 18.6.1). -/
@[simp] theorem eval_legendre_neg_one (n : ℕ) : (legendre R n).eval (-1) = (-1) ^ n := by
  rw [eval_legendre_neg, eval_legendre_one, mul_one]

Theorem 3.3.41 Legendre three-term recurrence

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). Then

\[ (n+2)P_{n+2}=(2n+3)XP_{n+1}-(n+1)P_n. \]

Reference: [DLMF, 18.9.1].

Lean Formalisation

theorem Polynomial.legendre_recurrence.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  Polynomial.C (↑n + 2) * Polynomial.legendre R (n + 2) =
    Polynomial.C (2 * ↑n + 3) * Polynomial.X * Polynomial.legendre R (n + 1) -
      Polynomial.C (↑n + 1) * Polynomial.legendre R n

Lean proof

/-- The cleared three-term recurrence over every commutative rational algebra
(DLMF Table 18.9.1). -/
theorem legendre_recurrence (R : Type*) [CommRing R] [Algebra ℚ R] (n : ℕ) :
    C (n + 2 : R) * legendre R (n + 2) =
      C (2 * n + 3 : R) * X * legendre R (n + 1) - C (n + 1 : R) * legendre R n := by
  have hq : C (n + 2 : ℚ) * legendre ℚ (n + 2) =
      C (2 * n + 3 : ℚ) * X * legendre ℚ (n + 1) - C (n + 1 : ℚ) * legendre ℚ n := by
    apply (map_injective (algebraMap ℚ ℝ) (algebraMap ℚ ℝ).injective)
    simpa only [Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_C,
      map_X, map_legendre_rat, map_add, map_mul, map_natCast, map_ofNat, map_one,
      Polynomial.map_add, Polynomial.map_natCast, Polynomial.map_ofNat, Polynomial.map_one] using
      legendre_recurrence_real n
  have h := congrArg (Polynomial.map (algebraMap ℚ R)) hq
  simpa only [Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_C,
    map_X, map_legendre_rat, map_add, map_mul, map_natCast, map_ofNat, map_one,
      Polynomial.map_add, Polynomial.map_natCast, Polynomial.map_ofNat, Polynomial.map_one] using h

Theorem 3.3.42 Legendre parity

✓ 🙂 human-reviewed

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). Then \(P_n(-X)=(-1)^nP_n(X)\).

Reference: [DLMF, Table 18.6.1].

Lean Formalisation

theorem Polynomial.legendre_comp_neg_X.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  (Polynomial.legendre R n).comp (-Polynomial.X) = Polynomial.C ((-1) ^ n) * Polynomial.legendre R n

Lean proof

/-- Legendre parity as a polynomial identity (DLMF Table 18.6.1). -/
theorem legendre_comp_neg_X (n : ℕ) :
    (legendre R n).comp (-X) = C ((-1 : R) ^ n) * legendre R n := by
  have hd := iterate_derivative_comp_affine R ((X ^ 2 - 1) ^ n) (-1) 0 n
  simp only [map_neg, map_one, map_zero, neg_one_mul, add_zero] at hd
  have hp : ((X ^ 2 - 1 : R[X]) ^ n).comp (-X) = (X ^ 2 - 1) ^ n := by
    simp only [pow_comp, sub_comp, X_comp, one_comp, neg_sq]
  rw [hp] at hd
  have hs : C ((-1 : R) ^ n) * C ((-1 : R) ^ n) = (1 : R[X]) := by
    rw [← C_mul, ← mul_pow]
    simp
  have he := congrArg (fun p : R[X] ↦ C ((-1 : R) ^ n) * p) hd
  rw [← mul_assoc, hs, one_mul] at he
  simp only [legendre, mul_comp, C_comp]
  rw [← he]
  ring

1 related Lean declaration

theorem Polynomial.eval_legendre_neg.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) (x : R) :
  Polynomial.eval (-x) (Polynomial.legendre R n) = (-1) ^ n * Polynomial.eval x (Polynomial.legendre R n)

Lean proof

/-- Legendre parity at every ring element (DLMF Table 18.6.1). -/
theorem eval_legendre_neg (n : ℕ) (x : R) :
    (legendre R n).eval (-x) = (-1) ^ n * (legendre R n).eval x := by
  have h := congrArg (fun p : R[X] ↦ p.eval x) (legendre_comp_neg_X R n)
  simpa only [eval_comp, eval_neg, eval_X, eval_mul, eval_C] using h

Theorem 3.3.43 Legendre degree and leading coefficient

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). The Legendre polynomial \(P_n(X)\in R[X]\) has degree at most \(n\), and its coefficient of \(X^n\) is \(2^{-n}\binom {2n}{n}\). If \(R\) is nontrivial, this coefficient is nonzero, \(P_n\) has degree exactly \(n\), and its leading coefficient is \(2^{-n}\binom {2n}{n}\). For nontrivial \(R\), the Legendre polynomials therefore form a degree-indexed polynomial sequence.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.degree_legendre_le.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  (Polynomial.legendre R n).degree ≤ ↑n

Lean proof

/-- The Legendre degree bound holds also in the trivial algebra (DLMF Table 18.3.1). -/
theorem degree_legendre_le (n : ℕ) : (legendre R n).degree ≤ n := by
  rw [legendre_eq_jacobi]
  exact degree_jacobi_le _ _ _

6 related Lean declarations

theorem Polynomial.coeff_legendre_self.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  (Polynomial.legendre R n).coeff n = (algebraMap ℚ R) (↑((2 * n).choose n) / 2 ^ n)

Lean proof

/-- The top coefficient is the central binomial coefficient divided by `2^n`
(DLMF Table 18.3.1). -/
theorem coeff_legendre_self (n : ℕ) :
    (legendre R n).coeff n = algebraMap ℚ R (((2 * n).choose n : ℚ) / 2 ^ n) := by
  rw [legendre_eq_jacobi, coeff_jacobi_self]
  simp only [add_zero]
  have hp : (ascPochhammer R n).eval ((n : R) + 1) =
      (n.factorial : R) * ((2 * n).choose n : R) := by
    rw [show (n : R) + 1 = ((n + 1 : ℕ) : R) by push_cast; rfl,
      ← Nat.cast_ascFactorial, Nat.ascFactorial_eq_factorial_mul_choose, ← two_mul, Nat.cast_mul]
  rw [hp]
  have h : (((n.factorial : ℚ) * 2 ^ n)⁻¹) *
      (n.factorial * ((2 * n).choose n : ℚ)) = ((2 * n).choose n : ℚ) / 2 ^ n := by
    field_simp
  simpa only [map_mul, map_natCast] using congrArg (algebraMap ℚ R) h

theorem Polynomial.degree_legendre.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] [Nontrivial R] (n : ℕ) :
  (Polynomial.legendre R n).degree = ↑n

Lean proof

/-- Legendre polynomials have exact degree in every nontrivial rational algebra
(DLMF Table 18.3.1). -/
@[simp] theorem degree_legendre [Nontrivial R] (n : ℕ) : (legendre R n).degree = n := by
  apply degree_eq_of_le_of_coeff_ne_zero (degree_legendre_le R n)
  rw [coeff_legendre_self]
  rw [← map_zero (algebraMap ℚ R)]
  apply (algebraMap ℚ R).injective.ne
  have hchoose : 0 < (2 * n).choose n := Nat.choose_pos (by omega)
  positivity

theorem Polynomial.natDegree_legendre.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] [Nontrivial R] (n : ℕ) :
  (Polynomial.legendre R n).natDegree = n

Lean proof

/-- The natural degree of a Legendre polynomial (DLMF Table 18.3.1). -/
@[simp] theorem natDegree_legendre [Nontrivial R] (n : ℕ) :
    (legendre R n).natDegree = n := natDegree_eq_of_degree_eq_some (degree_legendre R n)

theorem Polynomial.leadingCoeff_legendre.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] [Nontrivial R] (n : ℕ) :
  (Polynomial.legendre R n).leadingCoeff = (algebraMap ℚ R) (↑((2 * n).choose n) / 2 ^ n)

Lean proof

/-- The leading coefficient of a Legendre polynomial (DLMF Table 18.3.1). -/
theorem leadingCoeff_legendre [Nontrivial R] (n : ℕ) :
    (legendre R n).leadingCoeff = algebraMap ℚ R (((2 * n).choose n : ℚ) / 2 ^ n) := by
  rw [leadingCoeff, natDegree_legendre, coeff_legendre_self]

def Polynomial.legendreSequence.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] [Nontrivial R] : Polynomial.Sequence R

Lean definition

/-- The Legendre family as Mathlib's degree-indexed polynomial sequence
(DLMF Table 18.3.1). -/
@[expose] noncomputable def legendreSequence [Nontrivial R] : Polynomial.Sequence R where
  elems' := legendre R
  degree_eq' := degree_legendre R

theorem Polynomial.legendreSequence_apply.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] [Nontrivial R] (n : ℕ) :
  ↑(Polynomial.legendreSequence R) n = Polynomial.legendre R n

Lean proof

/-- The Legendre sequence uses the Rodrigues-defined family (DLMF Table 18.3.1). -/
@[simp] theorem legendreSequence_apply [Nontrivial R] (n : ℕ) :
    legendreSequence R n = legendre R n := rfl

Theorem 3.3.44 Legendre derivative

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). Then \(P_{n+1}'=(n+2)P_n^{(1,1)}/2\).

Reference: [DLMF, 18.9.15].

Lean Formalisation

theorem Polynomial.derivative_legendre_succ.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  Polynomial.derivative (Polynomial.legendre R (n + 1)) =
    Polynomial.C ((algebraMap ℚ R) (1 / 2) * (↑n + 2)) * Polynomial.jacobi 1 1 n

Lean proof

/-- Differentiating Legendre gives the shifted-parameter Jacobi family
(DLMF 18.9.15 at parameters zero). -/
theorem derivative_legendre_succ (n : ℕ) :
    derivative (legendre R (n + 1)) =
      C (algebraMap ℚ R (1 / 2) * ((n : R) + 2)) * jacobi (1 : R) 1 n := by
  rw [legendre_eq_jacobi, derivative_jacobi_succ]
  simp only [zero_add, add_zero]

Theorem 3.3.45 Legendre differential equation

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). The Legendre polynomials satisfy

\[ (1-X^2)P_n''-2XP_n'+n(n+1)P_n=0 \]

Reference: [DLMF, Table 18.8.1].

Lean Formalisation

theorem Polynomial.legendre_differentialEquation.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.derivative (Polynomial.legendre R n)) -
        2 * Polynomial.X * Polynomial.derivative (Polynomial.legendre R n) +
      Polynomial.C (↑n * (↑n + 1)) * Polynomial.legendre R n =
    0

Lean proof

/-- The Legendre differential equation as a polynomial identity (DLMF Table 18.8.1). -/
theorem legendre_differentialEquation (n : ℕ) :
    (1 - X ^ 2) * derivative (derivative (legendre R n)) -
      2 * X * derivative (legendre R n) + C ((n : R) * (n + 1)) * legendre R n = 0 := by
  rw [legendre_eq_jacobi]
  simpa only [sub_self, C_0, zero_add, add_zero, map_ofNat, zero_sub, neg_mul,
    sub_eq_add_neg] using jacobi_differentialEquation (0 : R) 0 n

Definition 3.3.46 Legendre measure

✓ 🙂 human-reviewed

#

Let \(\mu _L\) be Lebesgue measure restricted to \((-1,1]\), the Legendre weight one.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

def Polynomial.legendreMeasure : MeasureTheory.Measure ℝ

Lean definition

/-- The unit Legendre weight, restricted to `(-1,1]` (DLMF Table 18.3.1). -/
@[expose] noncomputable def legendreMeasure : Measure ℝ := volume.restrict (Ioc (-1) 1)

Theorem 3.3.47 Legendre squared norms and integral pairing

✓ 🤖

#

For every \(n\ge 0\),

\[ \int _{-1}^{1}P_n(x)^2\, dx=\frac{2}{2n+1}. \]

Consequently \(\int P_mP_n\, d\mu _L=\delta _{mn}\, 2/(2n+1)\), with the same formula for the interval integral.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integral_sq_legendre (n : ℕ) :
  ∫ (x : ℝ) in -1..1, Polynomial.eval x (Polynomial.legendre ℝ n) ^ 2 = 2 / (2 * ↑n + 1)

Lean proof

/-- The squared Legendre norm for the unit weight is `2/(2n+1)`
(DLMF Table 18.3.1). -/
theorem integral_sq_legendre (n : ℕ) :
    ∫ x in (-1 : ℝ)..1, (legendre ℝ n).eval x ^ 2 = 2 / (2 * (n : ℝ) + 1) := by
  have hd : (derivative (legendre ℝ n)).degree < (n + 1 : ℕ) := by
    exact degree_derivative_le.trans_lt (by rw [degree_legendre]; exact_mod_cast Nat.lt_succ_self n)
  have hz := integral_mul_legendre_eq_zero_of_degree_lt hd
  have hibp := intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt
    (legendre ℝ n).continuous.continuousOn (legendre ℝ (n + 1)).continuous.continuousOn
    (fun x _ ↦ (legendre ℝ n).hasDerivAt x)
    (fun x _ ↦ (legendre ℝ (n + 1)).hasDerivAt x)
    ((legendre ℝ n).derivative.continuous.intervalIntegrable (-1) 1)
    ((legendre ℝ (n + 1)).derivative.continuous.intervalIntegrable (-1) 1)
  have hboundary : (legendre ℝ n).eval 1 * (legendre ℝ (n + 1)).eval 1 -
      (legendre ℝ n).eval (-1) * (legendre ℝ (n + 1)).eval (-1) = 2 := by
    simp only [eval_legendre_one, eval_legendre_neg_one, pow_succ]
    rw [← mul_assoc, ← mul_pow]
    norm_num
  rw [hboundary, hz, sub_zero] at hibp
  have hr := integral_mul_legendre_eq_zero_of_degree_lt (degree_derivative_legendre_succ_sub n)
  have hi₁ : IntervalIntegrable (fun x ↦ (derivative (legendre ℝ (n + 1))).eval x *
      (legendre ℝ n).eval x) volume (-1) 1 := by
    exact ((legendre ℝ (n + 1)).derivative.continuous.mul (legendre ℝ n).continuous).intervalIntegrable _ _
  have hi₂ : IntervalIntegrable (fun x ↦ (2 * (n : ℝ) + 1) * (legendre ℝ n).eval x ^ 2)
      volume (-1) 1 := by
    exact (continuous_const.mul ((legendre ℝ n).continuous.pow 2)).intervalIntegrable _ _
  simp only [eval_sub, eval_mul, eval_C, sub_mul, mul_assoc, ← pow_two] at hr
  rw [intervalIntegral.integral_sub hi₁ hi₂, intervalIntegral.integral_const_mul] at hr
  have he : (∫ x in (-1 : ℝ)..1, (legendre ℝ n).eval x *
      (derivative (legendre ℝ (n + 1))).eval x) =
      ∫ x in (-1 : ℝ)..1, (derivative (legendre ℝ (n + 1))).eval x * (legendre ℝ n).eval x := by
    congr 1
    funext x
    ring
  rw [he] at hibp
  apply (eq_div_iff (by positivity : 2 * (n : ℝ) + 1 ≠ 0)).2
  nlinarith

3 related Lean declarations

theorem Polynomial.integral_sq_legendre_measure (n : ℕ) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.legendre ℝ n) ^ 2 ∂Polynomial.legendreMeasure = 2 / (2 * ↑n + 1)

Lean proof

/-- The diagonal norm also uses the Legendre measure directly (DLMF Table 18.3.1). -/
theorem integral_sq_legendre_measure (n : ℕ) :
    ∫ x, (legendre ℝ n).eval x ^ 2 ∂legendreMeasure = 2 / (2 * (n : ℝ) + 1) := by
  simpa only [legendreMeasure, intervalIntegral.integral_of_le (show (-1 : ℝ) ≤ 1 by norm_num)]
    using integral_sq_legendre n

theorem Polynomial.integral_mul_legendre (m n : ℕ) :
  ∫ (x : ℝ) in -1..1, Polynomial.eval x (Polynomial.legendre ℝ m) * Polynomial.eval x (Polynomial.legendre ℝ n) =
    if m = n then 2 / (2 * ↑n + 1) else 0

Lean proof

/-- The complete Legendre integral pairing (DLMF Table 18.3.1). -/
theorem integral_mul_legendre (m n : ℕ) :
    ∫ x in (-1 : ℝ)..1, (legendre ℝ m).eval x * (legendre ℝ n).eval x =
      if m = n then 2 / (2 * (n : ℝ) + 1) else 0 := by
  by_cases h : m = n
  · subst m
    simpa only [ite_true, ← pow_two] using integral_sq_legendre n
  · rw [ite_eq_right h]
    exact integral_mul_legendre_eq_zero h

theorem Polynomial.integral_mul_legendre_measure (m n : ℕ) :
  ∫ (x : ℝ),
      Polynomial.eval x (Polynomial.legendre ℝ m) *
        Polynomial.eval x (Polynomial.legendre ℝ n) ∂Polynomial.legendreMeasure =
    if m = n then 2 / (2 * ↑n + 1) else 0

Lean proof

/-- The complete pairing for the Legendre measure (DLMF Table 18.3.1). -/
theorem integral_mul_legendre_measure (m n : ℕ) :
    ∫ x, (legendre ℝ m).eval x * (legendre ℝ n).eval x ∂legendreMeasure =
      if m = n then 2 / (2 * (n : ℝ) + 1) else 0 := by
  simpa only [legendreMeasure, intervalIntegral.integral_of_le (show (-1 : ℝ) ≤ 1 by norm_num)]
    using integral_mul_legendre m n

Theorem 3.3.48 Legendre root location

✓ 🤖

#

Every real zero of \(P_n\) lies strictly in \((-1,1)\).

Reference: [DLMF, 18.2(vi)].

Lean Formalisation

theorem Polynomial.root_legendre_mem_Ioo {n : ℕ} {x : ℝ} (hx : Polynomial.eval x (Polynomial.legendre ℝ n) = 0) :
  x ∈ Set.Ioo (-1) 1

Lean proof

/-- Every Legendre root lies in the open interval `(-1,1)` (DLMF 18.2(vi)). -/
theorem root_legendre_mem_Ioo {n : ℕ} {x : ℝ} (hx : (legendre ℝ n).eval x = 0) :
    x ∈ Ioo (-1) 1 := by
  have hleft := neg_one_lt_root_legendre hx
  have hneg : (legendre ℝ n).eval (-x) = 0 := by rw [eval_legendre_neg, hx, mul_zero]
  have hright := neg_one_lt_root_legendre hneg
  exact ⟨hleft, by linarith⟩

Theorem 3.3.49 Legendre strict interlacing

✓ 🤖

#

Consecutive Legendre polynomials have no common zero. Between any two distinct zeros of either member lies a zero of the other. For \(n\ge 1\), \(P_{n+1}\) has two zeros \(a{\lt}b\) such that every zero of \(P_n\) lies strictly between \(a\) and \(b\).

Reference: [DLMF, 18.2(vi)].

Lean Formalisation

theorem Polynomial.not_eval_legendre_eq_zero_and_succ (n : ℕ) (x : ℝ) :
  ¬(Polynomial.eval x (Polynomial.legendre ℝ n) = 0 ∧ Polynomial.eval x (Polynomial.legendre ℝ (n + 1)) = 0)

Lean proof

/-- Consecutive Legendre polynomials have no common root (DLMF 18.2(vi)). -/
theorem not_eval_legendre_eq_zero_and_succ (n : ℕ) (x : ℝ) :
    ¬ ((legendre ℝ n).eval x = 0 ∧ (legendre ℝ (n + 1)).eval x = 0) :=
  isOrthogonal_legendreSequence.not_eval_eq_zero_and_succ hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure n x

3 related Lean declarations

theorem Polynomial.exists_root_legendre_succ_between (n : ℕ) {a b : ℝ} (hab : a < b)
  (ha : Polynomial.eval a (Polynomial.legendre ℝ n) = 0) (hb : Polynomial.eval b (Polynomial.legendre ℝ n) = 0) :
  ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.legendre ℝ (n + 1)) = 0

Lean proof

/-- Between distinct degree-`n` Legendre roots is a degree-`n+1` root (DLMF 18.2(vi)). -/
theorem exists_root_legendre_succ_between (n : ℕ) {a b : ℝ} (hab : a < b)
    (ha : (legendre ℝ n).eval a = 0) (hb : (legendre ℝ n).eval b = 0) :
    ∃ c ∈ Ioo a b, (legendre ℝ (n + 1)).eval c = 0 :=
  isOrthogonal_legendreSequence.exists_root_succ_between hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure n hab ha hb

theorem Polynomial.exists_root_legendre_between_succ (n : ℕ) {a b : ℝ} (hab : a < b)
  (ha : Polynomial.eval a (Polynomial.legendre ℝ (n + 1)) = 0)
  (hb : Polynomial.eval b (Polynomial.legendre ℝ (n + 1)) = 0) :
  ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.legendre ℝ n) = 0

Lean proof

/-- Between distinct degree-`n+1` Legendre roots is a degree-`n` root (DLMF 18.2(vi)). -/
theorem exists_root_legendre_between_succ (n : ℕ) {a b : ℝ} (hab : a < b)
    (ha : (legendre ℝ (n + 1)).eval a = 0) (hb : (legendre ℝ (n + 1)).eval b = 0) :
    ∃ c ∈ Ioo a b, (legendre ℝ n).eval c = 0 :=
  isOrthogonal_legendreSequence.exists_root_between_succ hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure n hab ha hb

theorem Polynomial.exists_outer_roots_legendre {n : ℕ} (hn : 1 ≤ n) :
  ∃ a b,
    a < b ∧
      Polynomial.eval a (Polynomial.legendre ℝ (n + 1)) = 0 ∧
        Polynomial.eval b (Polynomial.legendre ℝ (n + 1)) = 0 ∧
          ∀ (x : ℝ), Polynomial.eval x (Polynomial.legendre ℝ n) = 0 → a < x ∧ x < b

Lean proof

/-- The higher-degree Legendre member has both outermost roots (DLMF 18.2(vi)). -/
theorem exists_outer_roots_legendre {n : ℕ} (hn : 1 ≤ n) :
    ∃ a b : ℝ, a < b ∧ (legendre ℝ (n + 1)).eval a = 0 ∧
      (legendre ℝ (n + 1)).eval b = 0 ∧
      ∀ x : ℝ, (legendre ℝ n).eval x = 0 → a < x ∧ x < b :=
  isOrthogonal_legendreSequence.exists_outer_roots hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure hn

Definition 3.3.50 Legendre coefficients

✓ 🤖

#

For fixed \(n\), let \(f:\mathbb {R}\to \mathbb {R}\) satisfy \(fP_n\in L^1(\mu _L)\), with pointwise values retained. Define \(a_n(f)=\frac{2n+1}{2}\int f(x)P_n(x)\, d\mu _L(x)\).

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

def Polynomial.legendreCoefficient {n : ℕ}
  (f : Polynomial.IntegralCoefficientInput ℝ Polynomial.legendreMeasure (Polynomial.legendre ℝ n)) : ℝ

Lean definition

/-- Legendre expansion coefficients on the full classical product-integrability domain
(DLMF 18.2(viii) and Table 18.3.1). -/
@[expose] noncomputable def legendreCoefficient {n : ℕ}
    (f : IntegralCoefficientInput ℝ legendreMeasure (legendre ℝ n)) : ℝ :=
  ((2 * (n : ℝ) + 1) / 2) * ∫ x, f.val x * (legendre ℝ n).eval x ∂legendreMeasure

The map \(J_{\mu _L}\) sends a polynomial to its \(L^2(\mu _L)\) class. Convergence below is in this norm.

Theorem 3.3.51 Legendre L2 expansion

✓ 🤖

#

For every \(f\in L^2(\mu _L)\) the Hilbert-coordinate summands equal \(a_n(f)J_{\mu _L}P_n\), their series sums to \(f\), and \(\sum _{n=0}^{N-1}a_n(f)J_{\mu _L}P_n\to f\) in \(L^2\) as \(N\to \infty \).

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

theorem Polynomial.hilbertBasisLegendre_repr_smul (f : ↥(MeasureTheory.Lp ℝ 2 Polynomial.legendreMeasure)) (n : ℕ) :
  ↑(Polynomial.hilbertBasisLegendre.repr f) n • Polynomial.hilbertBasisLegendre n =
    Polynomial.legendreCoefficient (Polynomial.IntegralCoefficientInput.ofLegendreL2 f n) •
      (Polynomial.polynomialToL2 Polynomial.hasFiniteMoments_legendreMeasure) (Polynomial.legendre ℝ n)

Lean proof

/-- Hilbert-coordinate summands are the standard Legendre expansion terms
(DLMF 18.2(viii)). -/
theorem hilbertBasisLegendre_repr_smul (f : Lp ℝ 2 legendreMeasure) (n : ℕ) :
    hilbertBasisLegendre.repr f n • hilbertBasisLegendre n =
      legendreCoefficient (IntegralCoefficientInput.ofLegendreL2 f n) • polynomialToL2 hasFiniteMoments_legendreMeasure (legendre ℝ n) := by
  rw [HilbertBasis.repr_apply_apply, hilbertBasisLegendre_apply, normalizedLegendre,
    inner_smul_left, inner_polynomialToL2_left]
  simp only [conj_trivial, smul_smul]
  congr 1
  have hp : 0 ≤ 2 / (2 * (n : ℝ) + 1) := by positivity
  calc
    _ = ((√(2 / (2 * (n : ℝ) + 1)))⁻¹ * (√(2 / (2 * (n : ℝ) + 1)))⁻¹) *
        (∫ x, f x * (legendre ℝ n).eval x ∂legendreMeasure) := by ring
    _ = _ := by rw [← mul_inv, Real.mul_self_sqrt hp, inv_div]; rfl

2 related Lean declarations

theorem Polynomial.hasSum_legendreCoefficient_polynomialToL2 (f : ↥(MeasureTheory.Lp ℝ 2 Polynomial.legendreMeasure)) :
  HasSum
    (fun n =>
      Polynomial.legendreCoefficient (Polynomial.IntegralCoefficientInput.ofLegendreL2 f n) •
        (Polynomial.polynomialToL2 Polynomial.hasFiniteMoments_legendreMeasure) (Polynomial.legendre ℝ n))
    f

Lean proof

/-- Every unit-weight L² function is the L² sum of its Legendre expansion
(DLMF 18.2(viii)). -/
theorem hasSum_legendreCoefficient_polynomialToL2 (f : Lp ℝ 2 legendreMeasure) :
    HasSum (fun n : ℕ ↦ legendreCoefficient (IntegralCoefficientInput.ofLegendreL2 f n) •
      polynomialToL2 hasFiniteMoments_legendreMeasure (legendre ℝ n)) f := by
  simpa only [hilbertBasisLegendre_repr_smul] using hilbertBasisLegendre.hasSum_repr f

theorem Polynomial.tendsto_sum_legendreCoefficient_polynomialToL2 (f : ↥(MeasureTheory.Lp ℝ 2 Polynomial.legendreMeasure)) :
  Filter.Tendsto
    (fun N =>
      ∑ n ∈ Finset.range N,
        Polynomial.legendreCoefficient (Polynomial.IntegralCoefficientInput.ofLegendreL2 f n) •
          (Polynomial.polynomialToL2 Polynomial.hasFiniteMoments_legendreMeasure) (Polynomial.legendre ℝ n))
    Filter.atTop (nhds f)

Lean proof

/-- Natural-order Legendre partial sums converge in L² (DLMF 18.2(viii)). -/
theorem tendsto_sum_legendreCoefficient_polynomialToL2 (f : Lp ℝ 2 legendreMeasure) :
    Filter.Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.range N, legendreCoefficient (IntegralCoefficientInput.ofLegendreL2 f n) •
      polynomialToL2 hasFiniteMoments_legendreMeasure (legendre ℝ n)) atTop (nhds f) :=
  (hasSum_legendreCoefficient_polynomialToL2 f).tendsto_sum_nat

Coefficient maps, shifted polynomials and Legendre structure

Theorem 3.3.52 Legendre polynomials under coefficient maps

✓ 🤖

#

Let \(R,S\) be commutative \(\mathbb {Q}\)-algebras, let \(n\in \mathbb {N}\), and let \(f:R\to S\) be a \(\mathbb {Q}\)-algebra homomorphism. Applying \(f\) to the coefficients of \(P_n\) over \(R\) gives \(P_n\) over \(S\). In particular, \(P_n\) over \(R\) is the image of the rational polynomial \(P_n\).

Reference: [DLMF, 18.5.5].

Lean Formalisation

theorem Polynomial.map_legendre.{u_1, u_2} (R : Type u_1) [CommRing R] [Algebra ℚ R] {S : Type u_2} [CommRing S] [Algebra ℚ S]
  (f : R →ₐ[ℚ] S) (n : ℕ) : Polynomial.map f.toRingHom (Polynomial.legendre R n) = Polynomial.legendre S n

Lean proof

/-- Legendre polynomials commute with coefficient maps (DLMF 18.5.5). -/
theorem map_legendre {S : Type*} [CommRing S] [Algebra ℚ S] (f : R →ₐ[ℚ] S) (n : ℕ) :
    (legendre R n).map f.toRingHom = legendre S n := by
  simp only [legendre, Polynomial.map_mul, Polynomial.map_C,
    ← iterate_derivative_map, Polynomial.map_pow, Polynomial.map_sub, map_X,
    Polynomial.map_one]
  congr 2
  exact f.commutes _

1 related Lean declaration

theorem Polynomial.map_legendre_rat.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  Polynomial.map (algebraMap ℚ R) (Polynomial.legendre ℚ n) = Polynomial.legendre R n

Lean proof

/-- The rational-coefficient construction specialises to every rational algebra
(DLMF 18.5.5). -/
theorem map_legendre_rat (n : ℕ) :
    (legendre ℚ n).map (algebraMap ℚ R) = legendre R n :=
  map_legendre ℚ (Algebra.ofId ℚ R) n

Theorem 3.3.53 Legendre hypergeometric representation

✓ 🤖

#

For real or complex \(x\) and \(n\in \mathbb {N}\),

\[ P_n(x)={}_2F_1\! \left(-n,n+1;1;\frac{1-x}2\right), \]

where \({}_2F_1\) is the Gauss series of Definition 1.2.6. No hypothesis is needed.

Reference: [DLMF, 18.5.7], [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.eval_legendre_eq_ordinaryHypergeometric.{u_1} {𝕂 : Type u_1} [RCLike 𝕂] (x : 𝕂) (n : ℕ) :
  Polynomial.eval x (Polynomial.legendre 𝕂 n) =
    ordinaryHypergeometricOn (GaussParameters.ofTerminating (-↑n) (↑n + 1) 1 n ⋯ ⋯)
      (GaussSeriesPoint.ofTerminating (GaussParameters.ofTerminating (-↑n) (↑n + 1) 1 n ⋯ ⋯) n ⋯ ((1 - x) / 2))

Lean proof

/-- Legendre's classical terminating Gauss representation, at every argument. -/
theorem eval_legendre_eq_ordinaryHypergeometric {𝕂 : Type*} [RCLike 𝕂] (x : 𝕂) (n : ℕ) :
    (legendre 𝕂 n).eval x = ordinaryHypergeometricOn (GaussParameters.ofTerminating (-(n : 𝕂)) (n + 1) 1 n (Or.inl rfl)
        (by simpa only [ascPochhammer_eval_one] using (Nat.cast_ne_zero.mpr n.factorial_ne_zero : (n.factorial : 𝕂) ≠ 0)))
      (.ofTerminating _ n (Or.inl rfl) ((1 - x) / 2)) := by
  have hnf : (n.factorial : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)
  have h := eval_jacobi_eq_ordinaryHypergeometric (0 : 𝕂) 0 x n
    (by rwa [zero_add, ascPochhammer_eval_one])
  rw [ordinaryHypergeometricOn_terminating] at h ⊢
  simp only [ordinaryHypergeometricCoefficientOn, GaussParameters.ofTerminating] at h ⊢
  rw [legendre_eq_jacobi]
  simpa only [zero_add, ascPochhammer_eval_one, div_self hnf, one_mul,
    add_zero] using h

Theorem 3.3.54 Legendre and the reflected shifted family

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). After mapping the integer coefficients of the shifted Legendre polynomial \(S_n\) into \(R\),

\[ P_n(1-2X)=S_n(X),\qquad P_n(X)=S_n((1-X)/2). \]

Equivalently, \(P_n(2X-1)=(-1)^nS_n(X)\). The parity factor arises because \(S_n\) is oriented by \(S_1(X)=1-2X\).

Reference: [DLMF, 18.7.10 and Table 18.6.1].

Lean Formalisation

theorem Polynomial.legendre_comp_one_sub_two_mul_X.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  (Polynomial.legendre R n).comp (1 - 2 * Polynomial.X) =
    Polynomial.map (Int.castRingHom R) (Polynomial.shiftedLegendre n)

Lean proof

/-- Mathlib's shifted Legendre polynomial uses the orientation `1 - 2X`
(DLMF Table 18.3.1, with the shifted variable reversed). -/
theorem legendre_comp_one_sub_two_mul_X (n : ℕ) :
    (legendre R n).comp (1 - 2 * X) = (shiftedLegendre n).map (Int.castRingHom R) := by
  have h := congrArg (Polynomial.map (algebraMap ℚ R)) (legendre_comp_one_sub_two_mul_X_rat n)
  rw [Polynomial.map_comp, map_legendre_rat] at h
  have hm : (algebraMap ℚ R).comp (Int.castRingHom ℚ) = Int.castRingHom R := by
    ext z
    simp
  simpa only [Polynomial.map_sub, Polynomial.map_one, Polynomial.map_mul,
    Polynomial.map_ofNat, map_X, map_map, hm] using h

2 related Lean declarations

theorem Polynomial.legendre_eq_shiftedLegendre_comp.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  Polynomial.legendre R n =
    (Polynomial.map (Int.castRingHom R) (Polynomial.shiftedLegendre n)).comp
      (Polynomial.C ((algebraMap ℚ R) (1 / 2)) * (1 - Polynomial.X))

Lean proof

/-- Recover standard Legendre polynomials by undoing Mathlib's shift
(DLMF Table 18.3.1). -/
theorem legendre_eq_shiftedLegendre_comp (n : ℕ) :
    legendre R n = ((shiftedLegendre n).map (Int.castRingHom R)).comp
      (C (algebraMap ℚ R (1 / 2)) * (1 - X)) := by
  have h := congrArg (fun p : R[X] ↦ p.comp (C (algebraMap ℚ R (1 / 2)) * (1 - X)))
    (legendre_comp_one_sub_two_mul_X R n)
  have hh : (2 : R) * algebraMap ℚ R (1 / 2) = 1 := by
    have hh := congrArg (algebraMap ℚ R) (show (2 : ℚ) * (1 / 2) = 1 by norm_num)
    simpa only [map_mul, map_ofNat, map_one] using hh
  have ha : (1 - 2 * X : R[X]).comp (C (algebraMap ℚ R (1 / 2)) * (1 - X)) = X := by
    simp only [sub_comp, one_comp, mul_comp, ofNat_comp, X_comp]
    have hh' := congrArg (C : R →+* R[X]) hh
    simp only [map_mul, map_ofNat, map_one] at hh'
    linear_combination -(1 - X) * hh'
  simpa only [comp_assoc, ha, comp_X] using h

theorem Polynomial.legendre_comp_two_mul_X_sub_one.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  (Polynomial.legendre R n).comp (2 * Polynomial.X - 1) =
    Polynomial.C ((-1) ^ n) * Polynomial.map (Int.castRingHom R) (Polynomial.shiftedLegendre n)

Lean proof

/-- With the conventional shift `2X - 1`, Mathlib's family carries a parity
factor (DLMF Table 18.6.1). -/
theorem legendre_comp_two_mul_X_sub_one (n : ℕ) :
    (legendre R n).comp (2 * X - 1) =
      C ((-1 : R) ^ n) * (shiftedLegendre n).map (Int.castRingHom R) := by
  have h := congrArg (fun p : R[X] ↦ p.comp (1 - 2 * X)) (legendre_comp_neg_X R n)
  have ha : (-X : R[X]).comp (1 - 2 * X) = 2 * X - 1 := by simp
  simpa only [comp_assoc, ha, mul_comp, C_comp, legendre_comp_one_sub_two_mul_X] using h

Theorem 3.3.55 Leading coefficient after Legendre differentiation

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). Then

\[ [X^n]P_{n+1}'=(2n+1)[X^n]P_n. \]

Reference: [DLMF, 18.3 and 18.9].

Lean Formalisation

theorem Polynomial.coeff_derivative_legendre_succ.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  (Polynomial.derivative (Polynomial.legendre R (n + 1))).coeff n = (2 * ↑n + 1) * (Polynomial.legendre R n).coeff n

Lean proof

/-- The top derivative coefficient of Legendre polynomials (DLMF Table 18.3.1). -/
theorem coeff_derivative_legendre_succ (n : ℕ) :
    (derivative (legendre R (n + 1))).coeff n = (2 * (n : R) + 1) * (legendre R n).coeff n := by
  rw [coeff_derivative, coeff_legendre_self, coeff_legendre_self]
  have h : (((2 * (n + 1)).choose (n + 1) : ℚ) / 2 ^ (n + 1)) * (n + 1) =
      (2 * (n : ℚ) + 1) * (((2 * n).choose n : ℚ) / 2 ^ n) := by
    have hc := congrArg (fun k : ℕ ↦ (k : ℚ)) (Nat.succ_mul_centralBinom_succ n)
    simp only [Nat.centralBinom, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_ofNat] at hc
    rw [pow_succ]
    field_simp
    linear_combination hc
  have hm := congrArg (algebraMap ℚ R) h
  simpa only [map_mul, map_add, map_natCast, map_ofNat, map_one] using hm

Theorem 3.3.56 Shifted Legendre family Mathlib

✓

#

Define the integer polynomial

\[ S_n(X)=\sum _{k=0}^n(-1)^k\binom nk\binom {n+k}{n}X^k. \]

It has degree \(n\), satisfies \(n!S_n=(d/dX)^n[X^n(1-X)^n]\), and \((-1)^nS_n(1-X)=S_n(X)\). In particular \(S_1(X)=1-2X\): its orientation is opposite to the frequently used shifted convention \(P_n(2X-1)\).

Reference: [DLMF, 18.7.10], with the reflected orientation \(x\mapsto 1-x\).

Lean Formalisation

theorem Polynomial.coeff_shiftedLegendre (n k : ℕ) :
  (Polynomial.shiftedLegendre n).coeff k = (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)

Mathlib source

4 related Lean declarations

def Polynomial.shiftedLegendre (n : ℕ) : Polynomial ℤ

Mathlib source

theorem Polynomial.degree_shiftedLegendre (n : ℕ) : (Polynomial.shiftedLegendre n).degree = ↑n

Mathlib source

theorem Polynomial.factorial_mul_shiftedLegendre_eq (n : ℕ) :
  ↑n.factorial * Polynomial.shiftedLegendre n = (⇑Polynomial.derivative)^[n] (Polynomial.X ^ n * (1 - Polynomial.X) ^ n)

Mathlib source

theorem Polynomial.neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq (n : ℕ) :
  (-1) ^ n * (Polynomial.shiftedLegendre n).comp (1 - Polynomial.X) = Polynomial.shiftedLegendre n

Mathlib source

Theorem 3.3.57 Finite Legendre moments

✓ 🤖

#

Every real polynomial has integrable square with respect to \(\mu _L\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.hasFiniteMoments_legendreMeasure : Polynomial.HasFiniteMoments Polynomial.legendreMeasure

Lean proof

/-- Every polynomial square is integrable for the Legendre weight (DLMF Table 18.3.1). -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasFiniteMoments_legendreMeasure : HasFiniteMoments legendreMeasure := by
  intro p
  exact (p.continuous.pow 2).integrableOn_Icc.mono_set Ioc_subset_Icc_self

Theorem 3.3.58 Legendre orthogonality

✓ 🤖

#

For distinct \(m,n\ge 0\),

\[ \int _{-1}^{1}P_m(x)P_n(x)\, dx=0. \]

The Legendre polynomial sequence is orthogonal for \(\mu _L\) in the general IsOrthogonal API, including integrability of every pairwise product.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integral_mul_legendre_eq_zero {m n : ℕ} (hmn : m ≠ n) :
  ∫ (x : ℝ) in -1..1, Polynomial.eval x (Polynomial.legendre ℝ m) * Polynomial.eval x (Polynomial.legendre ℝ n) = 0

Lean proof

/-- Distinct Legendre polynomials are orthogonal on `[-1,1]` (DLMF Table 18.3.1). -/
theorem integral_mul_legendre_eq_zero {m n : ℕ} (hmn : m ≠ n) :
    ∫ x in (-1 : ℝ)..1, (legendre ℝ m).eval x * (legendre ℝ n).eval x = 0 := by
  have h := integral_mul_jacobi_eq_zero (α := 0) (β := 0) (by norm_num) (by norm_num) hmn
  simpa [← legendre_eq_jacobi, ← legendreMeasure_eq_jacobiMeasure, legendreMeasure,
    intervalIntegral.integral_of_le (show (-1 : ℝ) ≤ 1 by norm_num)] using h

1 related Lean declaration

theorem Polynomial.isOrthogonal_legendreSequence : (Polynomial.legendreSequence ℝ).IsOrthogonal Polynomial.legendreMeasure

Lean proof

/-- The Legendre sequence is orthogonal for its unit weight (DLMF Table 18.3.1). -/
theorem isOrthogonal_legendreSequence : (legendreSequence ℝ).IsOrthogonal legendreMeasure where
  integrable m n := hasFiniteMoments_legendreMeasure.integrable_mul _ _
  orthogonal m n hmn := by
    simpa only [legendreSequence_apply, legendreMeasure,
      intervalIntegral.integral_of_le (show (-1 : ℝ) ≤ 1 by norm_num)] using
      integral_mul_legendre_eq_zero hmn

Theorem 3.3.59 Legendre orthogonality to lower degrees

✓ 🤖

#

For every real polynomial \(q\) of degree less than \(n\), \(\int _{-1}^{1}q(x)P_n(x)\, dx=0\).

Reference: [DLMF, 18.2(i)].

Lean Formalisation

theorem Polynomial.integral_mul_legendre_eq_zero_of_degree_lt {p : Polynomial ℝ} {n : ℕ} (hp : p.degree < ↑n) :
  ∫ (x : ℝ) in -1..1, Polynomial.eval x p * Polynomial.eval x (Polynomial.legendre ℝ n) = 0

Lean proof

/-- Legendre polynomials are orthogonal to every polynomial of lower degree
(DLMF 18.2(i)). -/
theorem integral_mul_legendre_eq_zero_of_degree_lt {p : ℝ[X]} {n : ℕ}
    (hp : p.degree < n) : ∫ x in (-1 : ℝ)..1, p.eval x * (legendre ℝ n).eval x = 0 := by
  have h := isOrthogonal_legendreSequence.integralInner_eq_zero_of_degree_lt
    hasFiniteMoments_legendreMeasure hp
  simpa only [integralInner, legendreMeasure, legendreSequence_apply,
    intervalIntegral.integral_of_le (show (-1 : ℝ) ≤ 1 by norm_num)] using h

Theorem 3.3.60 Positive Legendre measure

✓ 🤖

#

The measure \(\mu _L\) is finite and \(\int p^2\, d\mu _L{\gt}0\) for every nonzero real polynomial \(p\).

Lean Formalisation

theorem Polynomial.hasPositiveDefiniteIntegral_legendreMeasure :
  Polynomial.HasPositiveDefiniteIntegral Polynomial.legendreMeasure

Lean proof

/-- The Legendre integral pairing is positive definite (DLMF 18.2(i)). -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasPositiveDefiniteIntegral_legendreMeasure : HasPositiveDefiniteIntegral legendreMeasure := by
  apply HasPositiveDefiniteIntegral.of_positive
  intro p hp
  obtain ⟨x, hx, hpx⟩ := exists_eval_ne_zero_Ioo hp (show (-1 : ℝ) < 1 by norm_num)
  have hi := intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
    (show (-1 : ℝ) < 1 by norm_num) continuous_const.continuousOn
    (p.continuous.pow 2).continuousOn (fun _ _ ↦ sq_nonneg _) ⟨x, Ioo_subset_Icc_self hx, sq_pos_of_ne_zero hpx⟩
  simpa only [intervalIntegral.integral_zero, intervalIntegral.integral_of_le (show (-1 : ℝ) ≤ 1 by norm_num),
    legendreMeasure, MeasureTheory.integral_zero, Pi.pow_apply] using hi

1 related Lean declaration

theorem Polynomial.isFiniteMeasure_legendreMeasure : MeasureTheory.IsFiniteMeasure Polynomial.legendreMeasure

Lean proof

/-- The Legendre weight is finite (DLMF Table 18.3.1). -/
instance isFiniteMeasure_legendreMeasure : IsFiniteMeasure legendreMeasure :=
  hasFiniteMoments_legendreMeasure.isFiniteMeasure

Theorem 3.3.61 Legendre recurrence coefficients

✓ 🤖

#

In the general recurrence convention, \(h_n=2/(2n+1)\), \(A_n=(n+1)/(2n+1)\), \(B_n=0\), and \(C_n=(n+1)/(2n+3)\).

Reference: [DLMF, 18.9.1 and Table 18.9.1].

Lean Formalisation

theorem Polynomial.squaredNorm_legendreSequence (n : ℕ) :
  (Polynomial.legendreSequence ℝ).squaredNorm Polynomial.legendreMeasure n ⋯ = 2 / (2 * ↑n + 1)

Lean proof

/-- The known Legendre squared norms in the general sequence API (DLMF Table 18.3.1). -/
theorem squaredNorm_legendreSequence (n : ℕ) :
    (legendreSequence ℝ).squaredNorm legendreMeasure n (Polynomial.Sequence.IntegrableSquare.of _ _) = 2 / (2 * (n : ℝ) + 1) := by
  simpa only [Sequence.squaredNorm, integralInner_self, legendreSequence_apply]
    using integral_sq_legendre_measure n

3 related Lean declarations

theorem Polynomial.recurrenceA_legendreSequence (n : ℕ) :
  (Polynomial.legendreSequence ℝ).recurrenceA n = (↑n + 1) / (2 * ↑n + 1)

Lean proof

/-- The forward Legendre recurrence coefficient (DLMF Table 18.9.1). -/
theorem recurrenceA_legendreSequence (n : ℕ) :
    (legendreSequence ℝ).recurrenceA n = (n + 1 : ℝ) / (2 * n + 1) := by
  have h := coeff_derivative_legendre_succ ℝ n
  rw [coeff_derivative] at h
  have hl : (legendre ℝ (n + 1)).leadingCoeff * (n + 1 : ℝ) =
      (2 * n + 1 : ℝ) * (legendre ℝ n).leadingCoeff := by
    simpa only [leadingCoeff, natDegree_legendre] using h
  unfold Sequence.recurrenceA
  simp only [legendreSequence_apply]
  apply (div_eq_div_iff (leadingCoeff_ne_zero.mpr ((legendreSequence ℝ).ne_zero (n + 1)))
    (by positivity : (2 * n + 1 : ℝ) ≠ 0)).2
  simp only [legendreSequence_apply]
  nlinarith [hl]

theorem Polynomial.recurrenceB_legendreSequence (n : ℕ) :
  (Polynomial.legendreSequence ℝ).recurrenceB Polynomial.legendreMeasure n ⋯ = 0

Lean proof

/-- The diagonal Legendre recurrence coefficient vanishes by parity (DLMF Table 18.9.1). -/
theorem recurrenceB_legendreSequence (n : ℕ) :
    (legendreSequence ℝ).recurrenceB legendreMeasure n (Sequence.RecurrenceBInput.of _ _ _) = 0 := by
  have hodd (x : ℝ) : (-x) * (legendre ℝ n).eval (-x) ^ 2 =
      -(x * (legendre ℝ n).eval x ^ 2) := by
    rw [eval_legendre_neg, mul_pow, ← pow_mul, Nat.mul_comm n 2, pow_mul]
    norm_num
  have hi := intervalIntegral.integral_comp_neg (a := (-1 : ℝ)) (b := 1)
    (fun x : ℝ ↦ x * (legendre ℝ n).eval x ^ 2)
  simp only [hodd, intervalIntegral.integral_neg, neg_neg] at hi
  have hz : ∫ x in (-1 : ℝ)..1, x * (legendre ℝ n).eval x ^ 2 = 0 := by linarith
  unfold Sequence.recurrenceB integralInner
  simp only [legendreSequence_apply, eval_mul, eval_X, mul_assoc, ← pow_two]
  have hz' : (∫ x, x * (legendre ℝ n).eval x ^ 2 ∂legendreMeasure) = 0 := by
    rw [legendreMeasure, ← intervalIntegral.integral_of_le (show (-1 : ℝ) ≤ 1 by norm_num), hz]
  rw [hz', zero_div]

theorem Polynomial.recurrenceC_legendreSequence (n : ℕ) :
  (Polynomial.legendreSequence ℝ).recurrenceC Polynomial.legendreMeasure n ⋯ = (↑n + 1) / (2 * ↑n + 3)

Lean proof

/-- The backward Legendre recurrence coefficient (DLMF Table 18.9.1). -/
theorem recurrenceC_legendreSequence (n : ℕ) :
    (legendreSequence ℝ).recurrenceC legendreMeasure n (Sequence.RecurrenceCInput.of _ _ _) = (n + 1 : ℝ) / (2 * n + 3) := by
  rw [Sequence.recurrenceC, recurrenceA_legendreSequence, squaredNorm_legendreSequence,
    squaredNorm_legendreSequence]
  push_cast
  field_simp
  ring

Theorem 3.3.62 Legendre Christoffel–Darboux identities

✓ 🤖

#

Set \(K_n(x,y)=\sum _{k=0}^n\frac{2k+1}{2}P_k(x)P_k(y)\). For real \(x,y\),

\[ (x-y)K_n(x,y)=\frac{n+1}{2}\bigl(P_{n+1}(x)P_n(y)-P_n(x)P_{n+1}(y)\bigr), \]

\[ K_n(x,x)=\frac{n+1}{2}\bigl(P_{n+1}'(x)P_n(x)-P_n'(x)P_{n+1}(x)\bigr). \]

Reference: [DLMF, 18.2.12–13].

Lean Formalisation

theorem Polynomial.legendre_christoffelDarboux (n : ℕ) (x y : ℝ) :
  (x - y) *
      ∑ k ∈ Finset.range (n + 1),
        (2 * ↑k + 1) / 2 * Polynomial.eval x (Polynomial.legendre ℝ k) * Polynomial.eval y (Polynomial.legendre ℝ k) =
    (↑n + 1) / 2 *
      (Polynomial.eval x (Polynomial.legendre ℝ (n + 1)) * Polynomial.eval y (Polynomial.legendre ℝ n) -
        Polynomial.eval x (Polynomial.legendre ℝ n) * Polynomial.eval y (Polynomial.legendre ℝ (n + 1)))

Lean proof

/-- The Legendre Christoffel–Darboux identity, with `x-y` cleared (DLMF 18.2.12). -/
theorem legendre_christoffelDarboux (n : ℕ) (x y : ℝ) :
    (x - y) * ∑ k ∈ Finset.range (n + 1), ((2 * k + 1 : ℝ) / 2) *
      (legendre ℝ k).eval x * (legendre ℝ k).eval y =
    ((n + 1 : ℝ) / 2) * ((legendre ℝ (n + 1)).eval x * (legendre ℝ n).eval y -
      (legendre ℝ n).eval x * (legendre ℝ (n + 1)).eval y) := by
  have h := isOrthogonal_legendreSequence.christoffelDarboux hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure n x y
  simp only [Sequence.kernel_of_positive (hasPositiveDefiniteIntegral_legendreMeasure) (legendreSequence ℝ), legendreSequence_apply, squaredNorm_legendreSequence,
    recurrenceA_legendreSequence] at h
  have hc : ((n + 1 : ℝ) / (2 * n + 1)) / (2 / (2 * n + 1)) = (n + 1) / 2 := by field_simp
  rw [hc] at h
  convert h using 2
  congr 1
  funext k
  field_simp

1 related Lean declaration

theorem Polynomial.legendre_christoffelDarboux_diag (n : ℕ) (x : ℝ) :
  ∑ k ∈ Finset.range (n + 1), (2 * ↑k + 1) / 2 * Polynomial.eval x (Polynomial.legendre ℝ k) ^ 2 =
    (↑n + 1) / 2 *
      (Polynomial.eval x (Polynomial.derivative (Polynomial.legendre ℝ (n + 1))) *
          Polynomial.eval x (Polynomial.legendre ℝ n) -
        Polynomial.eval x (Polynomial.derivative (Polynomial.legendre ℝ n)) *
          Polynomial.eval x (Polynomial.legendre ℝ (n + 1)))

Lean proof

/-- The diagonal Legendre Christoffel–Darboux identity (DLMF 18.2.13). -/
theorem legendre_christoffelDarboux_diag (n : ℕ) (x : ℝ) :
    (∑ k ∈ Finset.range (n + 1), ((2 * k + 1 : ℝ) / 2) * (legendre ℝ k).eval x ^ 2) =
    ((n + 1 : ℝ) / 2) * ((legendre ℝ (n + 1)).derivative.eval x * (legendre ℝ n).eval x -
      (legendre ℝ n).derivative.eval x * (legendre ℝ (n + 1)).eval x) := by
  have h := isOrthogonal_legendreSequence.christoffelDarboux_diag hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure n x
  simp only [Sequence.kernel_of_positive (hasPositiveDefiniteIntegral_legendreMeasure) (legendreSequence ℝ), legendreSequence_apply, squaredNorm_legendreSequence,
    recurrenceA_legendreSequence] at h
  have hc : ((n + 1 : ℝ) / (2 * n + 1)) / (2 / (2 * n + 1)) = (n + 1) / 2 := by field_simp
  rw [hc] at h
  convert h using 2
  field_simp

Theorem 3.3.63 Real simple Legendre zeros

✓ 🤖

#

\(P_n\) splits over \(\mathbb {R}\), is separable, and has exactly \(n\) roots counted with multiplicity, hence \(n\) distinct real zeros.

Reference: [DLMF, 18.2(vi)].

Lean Formalisation

theorem Polynomial.splits_legendre (n : ℕ) : (Polynomial.legendre ℝ n).Splits

Lean proof

/-- Legendre polynomials split into real linear factors (DLMF 18.2(vi)). -/
theorem splits_legendre (n : ℕ) : (legendre ℝ n).Splits :=
  isOrthogonal_legendreSequence.splits hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure n

2 related Lean declarations

theorem Polynomial.card_roots_legendre (n : ℕ) : (Polynomial.legendre ℝ n).roots.card = n

Lean proof

/-- A Legendre polynomial has exactly its degree many real roots (DLMF 18.2(vi)). -/
theorem card_roots_legendre (n : ℕ) : (legendre ℝ n).roots.card = n :=
  isOrthogonal_legendreSequence.card_roots hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure n

theorem Polynomial.separable_legendre (n : ℕ) : (Polynomial.legendre ℝ n).Separable

Lean proof

/-- Every Legendre root is simple (DLMF 18.2(vi)). -/
theorem separable_legendre (n : ℕ) : (legendre ℝ n).Separable :=
  isOrthogonal_legendreSequence.separable hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure n

Definition 3.3.64 Normalised Legendre classes

✓ 🤖

#

Define \(e_n=\sqrt{(2n+1)/2}\, J_{\mu _L}P_n\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

def Polynomial.normalizedLegendre (n : ℕ) : ↥(MeasureTheory.Lp ℝ 2 Polynomial.legendreMeasure)

Lean definition

/-- Normalised Legendre classes (DLMF Table 18.3.1). -/
noncomputable def normalizedLegendre (n : ℕ) : Lp ℝ 2 legendreMeasure :=
  (√(2 / (2 * (n : ℝ) + 1)))⁻¹ • polynomialToL2 hasFiniteMoments_legendreMeasure (legendre ℝ n)

Theorem 3.3.65 Legendre Hilbert basis

✓ 🤖

#

The family \((e_n)_{n\ge 0}\) is orthonormal with dense span in real \(L^2(\mu _L)\) and defines a Hilbert basis.

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

theorem Polynomial.ae_mem_Icc_legendreMeasure : ∀ᵐ (x : ℝ) ∂Polynomial.legendreMeasure, x ∈ Set.Icc (-1) 1

Lean proof

/-- The unit Legendre weight is concentrated on `[-1,1]` (DLMF Table 18.3.1). -/
theorem ae_mem_Icc_legendreMeasure : ∀ᵐ x ∂legendreMeasure, x ∈ Set.Icc (-1) 1 := by
  exact (ae_restrict_mem measurableSet_Ioc).mono (fun _ h ↦ Set.Ioc_subset_Icc_self h)

7 related Lean declarations

theorem Polynomial.polynomialToL2_legendre_denseRange :
  DenseRange ⇑(Polynomial.polynomialToL2 Polynomial.hasFiniteMoments_legendreMeasure)

Lean proof

/-- Polynomial evaluations are dense in Legendre L² (DLMF 18.2(viii)). -/
theorem polynomialToL2_legendre_denseRange :
    DenseRange (polynomialToL2 hasFiniteMoments_legendreMeasure) :=
  polynomialToL2_denseRange hasFiniteMoments_legendreMeasure (-1) 1 ae_mem_Icc_legendreMeasure

theorem Polynomial.inner_polynomialToL2_legendre (n m : ℕ) :
  inner ℝ ((Polynomial.polynomialToL2 Polynomial.hasFiniteMoments_legendreMeasure) (Polynomial.legendre ℝ n))
      ((Polynomial.polynomialToL2 Polynomial.hasFiniteMoments_legendreMeasure) (Polynomial.legendre ℝ m)) =
    if n = m then 2 / (2 * ↑n + 1) else 0

Lean proof

/-- The Legendre pairing in L² (DLMF Table 18.3.1). -/
theorem inner_polynomialToL2_legendre (n m : ℕ) :
    ⟪polynomialToL2 hasFiniteMoments_legendreMeasure (legendre ℝ n),
      polynomialToL2 hasFiniteMoments_legendreMeasure (legendre ℝ m)⟫_ℝ =
      if n = m then 2 / (2 * (n : ℝ) + 1) else 0 := by
  rw [inner_polynomialToL2, integral_mul_legendre_measure]
  split_ifs with h
  · subst m; rfl
  · rfl

theorem Polynomial.orthonormal_normalizedLegendre : Orthonormal ℝ Polynomial.normalizedLegendre

Lean proof

/-- The normalised Legendre family is orthonormal (DLMF Table 18.3.1). -/
theorem orthonormal_normalizedLegendre : Orthonormal ℝ normalizedLegendre := by
  rw [orthonormal_iff_ite]
  intro n m
  simp only [normalizedLegendre, inner_smul_left, inner_smul_right, conj_trivial,
    inner_polynomialToL2_legendre]
  by_cases h : n = m
  · subst m
    simp only [↓reduceIte]
    have hp : 0 < (2 / (2 * (n : ℝ) + 1) : ℝ) := by positivity
    calc
      _ = ((√(2 / (2 * (n : ℝ) + 1)))⁻¹ * (√(2 / (2 * (n : ℝ) + 1)))⁻¹) *
          (2 / (2 * (n : ℝ) + 1)) := by ring
      _ = 1 := by rw [← mul_inv, Real.mul_self_sqrt hp.le, inv_mul_cancel₀ hp.ne']
  · simp [h]

theorem Polynomial.span_polynomialToL2_legendre :
  Submodule.span ℝ
      (Set.range fun n =>
        (Polynomial.polynomialToL2 Polynomial.hasFiniteMoments_legendreMeasure) (Polynomial.legendre ℝ n)) =
    (Polynomial.polynomialToL2 Polynomial.hasFiniteMoments_legendreMeasure).range

Lean proof

/-- Legendre polynomial classes span the polynomial image in L² (DLMF 18.2(viii)). -/
theorem span_polynomialToL2_legendre :
    Submodule.span ℝ (Set.range (fun n : ℕ ↦ polynomialToL2 hasFiniteMoments_legendreMeasure (legendre ℝ n))) =
      LinearMap.range (polynomialToL2 hasFiniteMoments_legendreMeasure) := by
  have hs : Submodule.span ℝ (Set.range (fun n : ℕ ↦ legendre ℝ n)) = ⊤ := by
    apply (legendreSequence ℝ).span
    intro n
    apply isUnit_iff_ne_zero.mpr
    exact leadingCoeff_ne_zero.mpr ((legendreSequence ℝ).ne_zero n)
  simpa only [Submodule.map_span, ← Set.range_comp, Function.comp_def, Submodule.map_top]
    using congrArg (Submodule.map (polynomialToL2 hasFiniteMoments_legendreMeasure)) hs

theorem Polynomial.normalizedLegendre_dense_span :
  (Submodule.span ℝ (Set.range Polynomial.normalizedLegendre)).topologicalClosure = ⊤

Lean proof

/-- The normalised Legendre family has dense span (DLMF 18.2(viii)). -/
theorem normalizedLegendre_dense_span :
    (Submodule.span ℝ (Set.range normalizedLegendre)).topologicalClosure = ⊤ := by
  have hd : (Submodule.span ℝ (Set.range (fun n : ℕ ↦ polynomialToL2 hasFiniteMoments_legendreMeasure (legendre ℝ n)))).topologicalClosure = ⊤ := by
    rw [span_polynomialToL2_legendre]
    exact Submodule.dense_iff_topologicalClosure_eq_top.mp polynomialToL2_legendre_denseRange
  have hs : Submodule.span ℝ (Set.range (fun n : ℕ ↦ polynomialToL2 hasFiniteMoments_legendreMeasure (legendre ℝ n))) ≤
      Submodule.span ℝ (Set.range normalizedLegendre) := by
    apply Submodule.span_le.mpr
    rintro _ ⟨n, rfl⟩
    have hp : 0 < (2 / (2 * (n : ℝ) + 1) : ℝ) := by positivity
    have hz : √(2 / (2 * (n : ℝ) + 1)) ≠ 0 := (Real.sqrt_pos.mpr hp).ne'
    have hm := (Submodule.span ℝ (Set.range normalizedLegendre)).smul_mem
      (√(2 / (2 * (n : ℝ) + 1))) (Submodule.subset_span (Set.mem_range_self n))
    simpa only [SetLike.mem_coe, normalizedLegendre, smul_smul, mul_inv_cancel₀ hz, one_smul] using hm
  apply top_unique
  rw [← hd]
  exact Submodule.topologicalClosure_mono hs

def Polynomial.hilbertBasisLegendre : HilbertBasis ℕ ℝ ↥(MeasureTheory.Lp ℝ 2 Polynomial.legendreMeasure)

Lean definition

/-- The Legendre Hilbert basis of weighted L² (DLMF Table 18.3.1; DLMF 18.2(viii)). -/
noncomputable def hilbertBasisLegendre : HilbertBasis ℕ ℝ (Lp ℝ 2 legendreMeasure) :=
  HilbertBasis.mk orthonormal_normalizedLegendre (by rw [normalizedLegendre_dense_span])

theorem Polynomial.hilbertBasisLegendre_apply (n : ℕ) : Polynomial.hilbertBasisLegendre n = Polynomial.normalizedLegendre n

Lean proof

/-- The Hilbert basis vectors are the normalised Legendre classes (DLMF Table 18.3.1). -/
@[simp] theorem hilbertBasisLegendre_apply (n : ℕ) : hilbertBasisLegendre n = normalizedLegendre n := by
  exact congrFun (HilbertBasis.coe_mk _ _) n

Theorem 3.3.66 Legendre coefficient characterization

✓ 🤖

#

For every \(f\in L^2(\mu _L;\mathbb R)\) and \(n\in \mathbb {N}\), the product \(fP_n\) is \(\mu _L\)-integrable. More generally, for every real-valued function \(f:\mathbb R\to \mathbb R\) with \(fP_n\) integrable, its Legendre coefficient is

\[ a_n(f)=\frac{2n+1}{2}\int f(x)P_n(x)\, d\mu _L(x). \]

Lean Formalisation

theorem Polynomial.legendreCoefficient_apply {n : ℕ}
  (f : Polynomial.IntegralCoefficientInput ℝ Polynomial.legendreMeasure (Polynomial.legendre ℝ n)) :
  Polynomial.legendreCoefficient f =
    (2 * ↑n + 1) / 2 * ∫ (x : ℝ), f.val x * Polynomial.eval x (Polynomial.legendre ℝ n) ∂Polynomial.legendreMeasure

Lean proof

/-- The standard coefficient formula on its classical domain (DLMF 18.2(viii)). -/
theorem legendreCoefficient_apply {n : ℕ}
    (f : IntegralCoefficientInput ℝ legendreMeasure (legendre ℝ n)) :
    legendreCoefficient f = ((2 * (n : ℝ) + 1) / 2) *
      ∫ x, f.val x * (legendre ℝ n).eval x ∂legendreMeasure := rfl

1 related Lean declaration

def Polynomial.IntegralCoefficientInput.ofLegendreL2 (f : ↥(MeasureTheory.Lp ℝ 2 Polynomial.legendreMeasure)) (n : ℕ) :
  Polynomial.IntegralCoefficientInput ℝ Polynomial.legendreMeasure (Polynomial.legendre ℝ n)

Lean definition

/-- L2 data supply every classical Legendre coefficient (DLMF 18.2(viii)). -/
@[expose] noncomputable def IntegralCoefficientInput.ofLegendreL2
    (f : Lp ℝ 2 legendreMeasure) (n : ℕ) :
    IntegralCoefficientInput ℝ legendreMeasure (legendre ℝ n) :=
  IntegralCoefficientInput.ofL2 hasFiniteMoments_legendreMeasure
    hasPositiveDefiniteIntegral_legendreMeasure (legendre ℝ n)
    (by simpa using ((legendreSequence ℝ).ne_zero n)) f

3.3.4 Chebyshev as Jacobi cases

The first- and second-kind Chebyshev polynomials correspond to Jacobi parameters \(-1/2\) and \(1/2\). Their polynomial normalizations differ by explicit factors, while their measures agree exactly.

Theorem 3.3.67 Chebyshev differential equations and endpoint values Mathlib

✓

#

The polynomials \(T_n\) and \(U_n\) satisfy

\[ (1-X^2)T_n''-XT_n'+n^2T_n=0,\quad T_n(1)=1, \]

\[ (1-X^2)U_n''-3XU_n'+n(n+2)U_n=0,\quad U_n(1)=n+1. \]

These hold over every commutative ring and for every integer \(n\).

Reference: [DLMF, Tables 18.8.1 and 18.6.1].

Lean Formalisation

theorem Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T.{u_1} {R : Type u_1} [CommRing R] (n : ℤ) :
  (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[2] (Polynomial.Chebyshev.T R n) =
    Polynomial.X * Polynomial.derivative (Polynomial.Chebyshev.T R n) - ↑n ^ 2 * Polynomial.Chebyshev.T R n

Mathlib source

3 related Lean declarations

theorem Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U.{u_1} {R : Type u_1} [CommRing R] (n : ℤ) :
  (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[2] (Polynomial.Chebyshev.U R n) =
    3 * Polynomial.X * Polynomial.derivative (Polynomial.Chebyshev.U R n) - (↑n + 2) * ↑n * Polynomial.Chebyshev.U R n

Mathlib source

theorem Polynomial.Chebyshev.T_eval_one.{u_1} (R : Type u_1) [CommRing R] (n : ℤ) :
  Polynomial.eval 1 (Polynomial.Chebyshev.T R n) = 1

Mathlib source

theorem Polynomial.Chebyshev.U_eval_one.{u_1} (R : Type u_1) [CommRing R] (n : ℤ) :
  Polynomial.eval 1 (Polynomial.Chebyshev.U R n) = ↑n + 1

Mathlib source

Theorem 3.3.68 Chebyshev–Jacobi bridges

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra and let \(n\in \mathbb {N}\). Then

\[ P_n^{(-1/2,-1/2)}=\frac{(1/2)_n}{n!}T_n,\qquad (n+1)P_n^{(1/2,1/2)}=\frac{(3/2)_n}{n!}U_n. \]

Reference: [DLMF, 18.7.3–4].

Lean Formalisation

theorem Polynomial.jacobi_eq_chebyshev_T.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  Polynomial.jacobi ((algebraMap ℚ R) (-1 / 2)) ((algebraMap ℚ R) (-1 / 2)) n =
    Polynomial.C ((algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval ((algebraMap ℚ R) (1 / 2)) (ascPochhammer R n)) *
      Polynomial.Chebyshev.T R ↑n

Lean proof

/-- The first-kind Chebyshev bridge with its exact normalisation (DLMF 18.7.3). -/
theorem jacobi_eq_chebyshev_T (R : Type*) [CommRing R] [Algebra ℚ R] (n : ℕ) :
    jacobi (algebraMap ℚ R (-1 / 2)) (algebraMap ℚ R (-1 / 2)) n =
      C (algebraMap ℚ R ((n.factorial : ℚ)⁻¹) *
        (ascPochhammer R n).eval (algebraMap ℚ R (1 / 2))) * Chebyshev.T R n := by
  let f : ℚ →ₐ[ℚ] R := Algebra.ofId ℚ R
  have h := congrArg (Polynomial.map f.toRingHom) (jacobi_eq_T_rat n)
  have hp (x : ℚ) : f ((ascPochhammer ℚ n).eval x) = (ascPochhammer R n).eval (f x) := by
    rw [← ascPochhammer_map f.toRingHom, eval_map]
    exact (eval₂_at_apply f.toRingHom x).symm
  simp only [Polynomial.map_mul, Polynomial.map_C, map_jacobi, Chebyshev.map_T] at h
  simp only [eval_jacobi_one] at h
  norm_num at h
  simpa only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, map_mul, hp, f,
    Algebra.ofId_apply, neg_div, map_neg] using h

1 related Lean declaration

theorem Polynomial.jacobi_eq_chebyshev_U.{u_1} (R : Type u_1) [CommRing R] [Algebra ℚ R] (n : ℕ) :
  Polynomial.C (↑n + 1) * Polynomial.jacobi ((algebraMap ℚ R) (1 / 2)) ((algebraMap ℚ R) (1 / 2)) n =
    Polynomial.C ((algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval ((algebraMap ℚ R) (3 / 2)) (ascPochhammer R n)) *
      Polynomial.Chebyshev.U R ↑n

Lean proof

/-- The second-kind Chebyshev bridge with its exact normalisation (DLMF 18.7.4). -/
theorem jacobi_eq_chebyshev_U (R : Type*) [CommRing R] [Algebra ℚ R] (n : ℕ) :
    C (n + 1 : R) * jacobi (algebraMap ℚ R (1 / 2)) (algebraMap ℚ R (1 / 2)) n =
      C (algebraMap ℚ R ((n.factorial : ℚ)⁻¹) *
        (ascPochhammer R n).eval (algebraMap ℚ R (3 / 2))) * Chebyshev.U R n := by
  let f : ℚ →ₐ[ℚ] R := Algebra.ofId ℚ R
  have h := congrArg (Polynomial.map f.toRingHom) (jacobi_eq_U_rat n)
  have hp (x : ℚ) : f ((ascPochhammer ℚ n).eval x) = (ascPochhammer R n).eval (f x) := by
    rw [← ascPochhammer_map f.toRingHom, eval_map]
    exact (eval₂_at_apply f.toRingHom x).symm
  simp only [Polynomial.map_mul, Polynomial.map_C, map_jacobi, Chebyshev.map_U] at h
  simp only [eval_jacobi_one] at h
  norm_num at h
  simpa only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, map_mul, hp,
    map_add, map_natCast, map_one, f, Algebra.ofId_apply] using h

Theorem 3.3.69 Classical Jacobi measure bridges

✓ 🤖

#

The existing measures satisfy

\[ \mu _L=\mu _{0,0},\qquad \mu _T=\mu _{-1/2,-1/2},\qquad \mu _U=\mu _{1/2,1/2}. \]

These are exact measure equalities, with no scalar normalization factor. Endpoints have zero mass, and restricting the measures to the open or half-open interval gives the same measure.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.legendreMeasure_eq_jacobiMeasure : Polynomial.legendreMeasure = Polynomial.jacobiMeasure 0 0

Lean proof

/-- The unit Legendre measure is the zero-parameter Jacobi measure
(DLMF Table 18.3.1). -/
theorem legendreMeasure_eq_jacobiMeasure : legendreMeasure = jacobiMeasure 0 0 := by
  have h : jacobiMeasure 0 0 = (volume.restrict (Ioo (-1 : ℝ) 1)).withDensity
      (fun _ ↦ 1) := by
    apply openIntervalWeightMeasure_eq _ _ _ _ measurable_const
    intro x
    simp [jacobiWeight]
    rfl
  simpa [legendreMeasure, restrict_Ioo_eq_restrict_Ioc] using h.symm

2 related Lean declarations

theorem Polynomial.measureT_eq_jacobiMeasure :
  Polynomial.Chebyshev.classicalMeasureT = Polynomial.jacobiMeasure (-1 / 2) (-1 / 2)

Lean proof

/-- The first-kind Chebyshev measure is the symmetric Jacobi negative-half measure. -/
theorem measureT_eq_jacobiMeasure :
    Chebyshev.classicalMeasureT = jacobiMeasure (-1 / 2) (-1 / 2) := by
  change openIntervalWeightMeasure (-1) 1 Chebyshev.weightT =
    openIntervalWeightMeasure (-1) 1 (jacobiWeight (-1 / 2) (-1 / 2))
  congr 1
  ext x
  rw [(Chebyshev.weightUT_apply x).2, jacobiWeight_apply]
  rw [← mul_rpow (by linarith [x.property.2] : 0 ≤ 1 - (x : ℝ))
    (by linarith [x.property.1] : 0 ≤ 1 + (x : ℝ))]
  rw [show (-1 / 2 : ℝ) = -(1 / 2) by ring,
    rpow_neg (mul_nonneg (by linarith [x.property.2]) (by linarith [x.property.1])),
    ← sqrt_eq_rpow]
  congr 2
  ring

theorem Polynomial.measureU_eq_jacobiMeasure : Polynomial.Chebyshev.measureU = Polynomial.jacobiMeasure (1 / 2) (1 / 2)

Lean proof

/-- The second-kind Chebyshev measure is the symmetric Jacobi half-parameter measure. -/
theorem measureU_eq_jacobiMeasure :
    Chebyshev.measureU = jacobiMeasure (1 / 2) (1 / 2) := by
  change openIntervalWeightMeasure (-1) 1 Chebyshev.weightU =
    openIntervalWeightMeasure (-1) 1 (jacobiWeight (1 / 2) (1 / 2))
  congr 1
  ext x
  rw [(Chebyshev.weightUT_apply x).1, jacobiWeight_apply]
  rw [← mul_rpow (by linarith [x.property.2] : 0 ≤ 1 - (x : ℝ))
    (by linarith [x.property.1] : 0 ≤ 1 + (x : ℝ)), ← sqrt_eq_rpow]
  congr 1
  ring

Hypergeometric representations and norm compatibility

Theorem 3.3.70 Chebyshev hypergeometric representations

✓ 🤖

#

For real or complex \(x\) and \(n\in \mathbb {N}\),

\[ T_n(x)={}_2F_1\! \left(-n,n;\tfrac 12;\frac{1-x}2\right),\qquad U_n(x)=(n+1)\, {}_2F_1\! \left(-n,n+2;\tfrac 32;\frac{1-x}2\right), \]

where \({}_2F_1\) is the Gauss series of Definition 1.2.6. No hypothesis is needed.

Reference: [DLMF, 18.5.11_2 and 18.5.11_4].

Lean Formalisation

theorem Polynomial.eval_chebyshev_T_eq_ordinaryHypergeometric.{u_1} {𝕂 : Type u_1} [RCLike 𝕂] (x : 𝕂) (n : ℕ) :
  Polynomial.eval x (Polynomial.Chebyshev.T 𝕂 ↑n) =
    ordinaryHypergeometricOn (GaussParameters.ofTerminating (-↑n) (↑n) (1 / 2) n ⋯ ⋯)
      (GaussSeriesPoint.ofTerminating (GaussParameters.ofTerminating (-↑n) (↑n) (1 / 2) n ⋯ ⋯) n ⋯ ((1 - x) / 2))

Lean proof

/-- Chebyshev's classical terminating Gauss representation, at every argument. -/
theorem eval_chebyshev_T_eq_ordinaryHypergeometric (x : 𝕂) (n : ℕ) :
    (Chebyshev.T 𝕂 n).eval x = ordinaryHypergeometricOn (GaussParameters.ofTerminating (-(n : 𝕂)) n (1 / 2) n (Or.inl rfl)
        (by have h := ascPochhammer_eval_ofReal_ne_zero (𝕂 := 𝕂) n (r := 1 / 2) (by norm_num); push_cast at h; exact h))
      (.ofTerminating _ n (Or.inl rfl) ((1 - x) / 2)) := by
  have hh : (ascPochhammer 𝕂 n).eval (1 / 2) ≠ 0 := by
    have h := ascPochhammer_eval_ofReal_ne_zero (𝕂 := 𝕂) n (r := 1 / 2) (by norm_num)
    push_cast at h
    exact h
  have hj := eval_jacobi_eq_ordinaryHypergeometric (-1 / 2 : 𝕂) (-1 / 2) x n
    (by rwa [show (-1 / 2 : 𝕂) + 1 = 1 / 2 by norm_num])
  rw [ordinaryHypergeometricOn_terminating] at hj ⊢
  simp only [ordinaryHypergeometricCoefficientOn, GaussParameters.ofTerminating] at hj ⊢
  have hb := congrArg (eval x) (jacobi_eq_chebyshev_T 𝕂 n)
  simp only [eval_mul, eval_C, map_div₀, map_neg, map_one, map_ofNat, map_inv₀,
    map_natCast] at hb
  simp only [show (-1 / 2 : 𝕂) + 1 = 1 / 2 by norm_num,
    show (n : 𝕂) + -1 / 2 + -1 / 2 + 1 = n by ring] at hj
  rw [hb] at hj
  have hnf : (n.factorial : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)
  apply mul_left_cancel₀ (mul_ne_zero (inv_ne_zero hnf) hh)
  rw [hj]
  field_simp
  apply Finset.sum_congr rfl
  intro k hk
  by_cases h : (ascPochhammer 𝕂 k).eval (-(n : 𝕂)) * (ascPochhammer 𝕂 k).eval (n : 𝕂) = 0
  · simp only [h, ite_true]
  · simp only [h, ite_false]

1 related Lean declaration

theorem Polynomial.eval_chebyshev_U_eq_ordinaryHypergeometric.{u_1} {𝕂 : Type u_1} [RCLike 𝕂] (x : 𝕂) (n : ℕ) :
  Polynomial.eval x (Polynomial.Chebyshev.U 𝕂 ↑n) =
    (↑n + 1) *
      ordinaryHypergeometricOn (GaussParameters.ofTerminating (-↑n) (↑n + 2) (3 / 2) n ⋯ ⋯)
        (GaussSeriesPoint.ofTerminating (GaussParameters.ofTerminating (-↑n) (↑n + 2) (3 / 2) n ⋯ ⋯) n ⋯ ((1 - x) / 2))

Lean proof

/-- Chebyshev's classical terminating Gauss representation, at every argument. -/
theorem eval_chebyshev_U_eq_ordinaryHypergeometric (x : 𝕂) (n : ℕ) :
    (Chebyshev.U 𝕂 n).eval x = (n + 1) * ordinaryHypergeometricOn (GaussParameters.ofTerminating (-(n : 𝕂)) (n + 2) (3 / 2) n (Or.inl rfl)
        (by have h := ascPochhammer_eval_ofReal_ne_zero (𝕂 := 𝕂) n (r := 3 / 2) (by norm_num); push_cast at h; exact h))
      (.ofTerminating _ n (Or.inl rfl) ((1 - x) / 2)) := by
  have hh : (ascPochhammer 𝕂 n).eval (3 / 2) ≠ 0 := by
    have h := ascPochhammer_eval_ofReal_ne_zero (𝕂 := 𝕂) n (r := 3 / 2) (by norm_num)
    push_cast at h
    exact h
  have hj := eval_jacobi_eq_ordinaryHypergeometric (1 / 2 : 𝕂) (1 / 2) x n
    (by rwa [show (1 / 2 : 𝕂) + 1 = 3 / 2 by norm_num])
  rw [ordinaryHypergeometricOn_terminating] at hj ⊢
  simp only [ordinaryHypergeometricCoefficientOn, GaussParameters.ofTerminating] at hj ⊢
  have hb := congrArg (eval x) (jacobi_eq_chebyshev_U 𝕂 n)
  simp only [eval_mul, eval_C, map_div₀, map_one, map_ofNat, map_inv₀, map_natCast] at hb
  simp only [show (1 / 2 : 𝕂) + 1 = 3 / 2 by norm_num,
    show (n : 𝕂) + 1 / 2 + 1 / 2 + 1 = n + 2 by ring] at hj
  rw [hj] at hb
  have hnf : (n.factorial : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)
  apply mul_left_cancel₀ (mul_ne_zero (inv_ne_zero hnf) hh)
  rw [← hb]
  field_simp
  apply Finset.sum_congr rfl
  intro k hk
  by_cases h : (ascPochhammer 𝕂 k).eval (-(n : 𝕂)) * (ascPochhammer 𝕂 k).eval ((n : 𝕂) + 2) = 0
  · simp only [h, ite_true]
  · simp only [h, ite_false]

Theorem 3.3.71 Classical norm compatibility

✓ 🤖

#

In the corresponding Jacobi measures, the squared norms of \(P_n^{(0,0)}\), \(T_n\) and \(U_n\) are respectively \(2/(2n+1)\), \(\pi \) for \(n=0\) and \(\pi /2\) otherwise, and \(\pi /2\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integral_sq_jacobi_zero_zero (n : ℕ) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.jacobi 0 0 n) ^ 2 ∂Polynomial.jacobiMeasure 0 0 = 2 / (2 * ↑n + 1)

Lean proof

/-- Legendre normalization transported to the Jacobi measure (DLMF Table 18.3.1). -/
theorem integral_sq_jacobi_zero_zero (n : ℕ) :
    ∫ x, (jacobi (0 : ℝ) 0 n).eval x ^ 2 ∂jacobiMeasure 0 0 =
      2 / (2 * (n : ℝ) + 1) := by
  rw [← legendreMeasure_eq_jacobiMeasure, ← legendre_eq_jacobi]
  exact integral_sq_legendre_measure n

2 related Lean declarations

theorem Polynomial.integral_sq_chebyshev_T_jacobiMeasure (n : ℕ) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) ^ 2 ∂Polynomial.jacobiMeasure (-1 / 2) (-1 / 2) =
    if n = 0 then Real.pi else Real.pi / 2

Lean proof

/-- The first-kind Chebyshev normalization, including its exceptional constant term. -/
theorem integral_sq_chebyshev_T_jacobiMeasure (n : ℕ) :
    ∫ x, (Chebyshev.T ℝ n).eval x ^ 2 ∂jacobiMeasure (-1 / 2) (-1 / 2) =
      if n = 0 then π else π / 2 := by
  rw [← measureT_eq_jacobiMeasure, Chebyshev.classicalMeasureT_eq]
  by_cases hn : n = 0
  · subst n
    simpa only [pow_two, Nat.cast_zero, ite_true] using
      Chebyshev.integral_eval_T_real_mul_self_measureT_zero
  · simpa only [pow_two, ite_eq_right hn] using
      Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero hn

theorem Polynomial.integral_sq_chebyshev_U_jacobiMeasure (n : ℕ) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.U ℝ ↑n) ^ 2 ∂Polynomial.jacobiMeasure (1 / 2) (1 / 2) = Real.pi / 2

Lean proof

/-- The second-kind Chebyshev normalization in Jacobi-measure form. -/
theorem integral_sq_chebyshev_U_jacobiMeasure (n : ℕ) :
    ∫ x, (Chebyshev.U ℝ n).eval x ^ 2 ∂jacobiMeasure (1 / 2) (1 / 2) = π / 2 := by
  rw [← measureU_eq_jacobiMeasure]
  simpa only [pow_two] using Chebyshev.integral_eval_U_real_mul_self_measureU n