LeanFun RevOLVER

3.2 Jacobi polynomials

Jacobi polynomials organize the classical families on \([-1,1]\). Algebraic formulas allow arbitrary parameters; orthogonality and weighted expansions use \(\alpha ,\beta {\gt}-1\).

3.2.1 Definition and normalization

The finite-sum definition is polynomial in the parameters and works over any commutative \(\mathbb {Q}\)-algebra, including \(\mathbb {Q}\), \(\mathbb {R}\) and \(\mathbb {C}\). Some parameter choices lower the degree; the leading-coefficient theorem states exactly when this happens.

Definition 3.2.1 Jacobi polynomials

✓ 🙂 human-reviewed

#

For a commutative \(\mathbb {Q}\)-algebra \(R\), \(\alpha ,\beta \in R\), and \(n\in \mathbb {N}\), define

\[ P_n^{(\alpha ,\beta )}(X)=\sum _{\ell =0}^n \frac{(n+\alpha +\beta +1)_\ell (\alpha +\ell +1)_{n-\ell }}{\ell !(n-\ell )!2^\ell }(X-1)^\ell . \]

Reference: [DLMF, 18.5.7].

Lean Formalisation

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

Lean definition

/-- Jacobi polynomials in DLMF normalisation (DLMF 18.5.7). -/
noncomputable def jacobi (α β : R) (n : ℕ) : R[X] :=
  ∑ l ∈ Finset.range (n + 1),
    C (algebraMap ℚ R (((l.factorial : ℚ) * (n - l).factorial * 2 ^ l)⁻¹) *
      (ascPochhammer R l).eval ((n : R) + α + β + 1) *
      (ascPochhammer R (n - l)).eval (α + l + 1)) * (X - 1) ^ l

Theorem 3.2.2 Degree and leading term

✓ 🙂 human-reviewed

#

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

\[ c_n=\frac{(n+\alpha +\beta +1)_n}{2^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_jacobi_le.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ) :
  (Polynomial.jacobi α β n).natDegree ≤ n

Lean proof

/-- The natural degree never exceeds the index (DLMF Table 18.3.1). -/
theorem natDegree_jacobi_le (α β : R) (n : ℕ) : (jacobi α β n).natDegree ≤ n := by
  nontriviality R
  unfold jacobi
  apply natDegree_sum_le_of_forall_le
  intro l hl
  apply (natDegree_C_mul_le _ _).trans
  have hpow : ((X - 1 : R[X]) ^ l).natDegree = l := by
    rw [← C_1, (monic_X_sub_C (1 : R)).natDegree_pow, natDegree_X_sub_C, mul_one]
  rw [hpow]
  exact Nat.le_of_lt_succ (Finset.mem_range.mp hl)

5 related Lean declarations

theorem Polynomial.degree_jacobi_le.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ) :
  (Polynomial.jacobi α β n).degree ≤ ↑n

Lean proof

/-- The degree bound also handles the zero polynomial (DLMF Table 18.3.1). -/
theorem degree_jacobi_le (α β : R) (n : ℕ) : (jacobi α β n).degree ≤ n :=
  degree_le_of_natDegree_le (natDegree_jacobi_le α β n)

theorem Polynomial.coeff_jacobi_self.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ) :
  (Polynomial.jacobi α β n).coeff n =
    (algebraMap ℚ R) (↑n.factorial * 2 ^ n)⁻¹ * Polynomial.eval (↑n + α + β + 1) (ascPochhammer R n)

Lean proof

/-- The coefficient of the potentially leading term (DLMF Table 18.3.1). -/
theorem coeff_jacobi_self (α β : R) (n : ℕ) :
    (jacobi α β n).coeff n =
      algebraMap ℚ R (((n.factorial : ℚ) * 2 ^ n)⁻¹) *
        (ascPochhammer R n).eval ((n : R) + α + β + 1) := by
  nontriviality R
  unfold jacobi
  rw [finsetSum_coeff, Finset.sum_eq_single n]
  · have hpow : ((X - 1 : R[X]) ^ n).coeff n = 1 := by
      have hd : ((X - 1 : R[X]) ^ n).natDegree = n := by
        rw [← C_1, (monic_X_sub_C (1 : R)).natDegree_pow, natDegree_X_sub_C, mul_one]
      simpa [hd] using ((monic_X_sub_C (1 : R)).pow n).coeff_natDegree
    simp only [coeff_C_mul, hpow, Nat.sub_self, ascPochhammer_zero, eval_one,
      mul_one, Nat.factorial_zero, Nat.cast_one]
  · intro l hl hln
    rw [coeff_C_mul, coeff_eq_zero_of_natDegree_lt, mul_zero]
    have hd : ((X - 1 : R[X]) ^ l).natDegree = l := by
      rw [← C_1, (monic_X_sub_C (1 : R)).natDegree_pow, natDegree_X_sub_C, mul_one]
    rw [hd]
    have := Finset.mem_range.mp hl
    omega
  · simp

theorem Polynomial.degree_jacobi_eq.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ)
  (h : (algebraMap ℚ R) (↑n.factorial * 2 ^ n)⁻¹ * Polynomial.eval (↑n + α + β + 1) (ascPochhammer R n) ≠ 0) :
  (Polynomial.jacobi α β n).degree = ↑n

Lean proof

/-- Nonvanishing of the top coefficient gives exact degree, including over rings
with zero divisors (DLMF Table 18.3.1). -/
theorem degree_jacobi_eq (α β : R) (n : ℕ)
    (h : algebraMap ℚ R (((n.factorial : ℚ) * 2 ^ n)⁻¹) *
      (ascPochhammer R n).eval ((n : R) + α + β + 1) ≠ 0) :
    (jacobi α β n).degree = n :=
  degree_eq_of_le_of_coeff_ne_zero (degree_jacobi_le α β n)
    (by rwa [coeff_jacobi_self])

theorem Polynomial.degree_jacobi_eq_iff.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ) :
  (Polynomial.jacobi α β n).degree = ↑n ↔
    (algebraMap ℚ R) (↑n.factorial * 2 ^ n)⁻¹ * Polynomial.eval (↑n + α + β + 1) (ascPochhammer R n) ≠ 0

Lean proof

/-- Exact degree is equivalent to the explicit nondegeneracy condition
(DLMF Table 18.3.1). -/
theorem degree_jacobi_eq_iff (α β : R) (n : ℕ) :
    (jacobi α β n).degree = n ↔
      algebraMap ℚ R (((n.factorial : ℚ) * 2 ^ n)⁻¹) *
        (ascPochhammer R n).eval ((n : R) + α + β + 1) ≠ 0 := by
  constructor
  · intro h
    rw [← coeff_jacobi_self]
    exact coeff_ne_zero_of_eq_degree h
  · exact degree_jacobi_eq α β n

theorem Polynomial.leadingCoeff_jacobi.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ)
  (h : (algebraMap ℚ R) (↑n.factorial * 2 ^ n)⁻¹ * Polynomial.eval (↑n + α + β + 1) (ascPochhammer R n) ≠ 0) :
  (Polynomial.jacobi α β n).leadingCoeff =
    (algebraMap ℚ R) (↑n.factorial * 2 ^ n)⁻¹ * Polynomial.eval (↑n + α + β + 1) (ascPochhammer R n)

Lean proof

/-- The leading coefficient in the nondegenerate case (DLMF Table 18.3.1). -/
theorem leadingCoeff_jacobi (α β : R) (n : ℕ)
    (h : algebraMap ℚ R (((n.factorial : ℚ) * 2 ^ n)⁻¹) *
      (ascPochhammer R n).eval ((n : R) + α + β + 1) ≠ 0) :
    (jacobi α β n).leadingCoeff = algebraMap ℚ R (((n.factorial : ℚ) * 2 ^ n)⁻¹) *
      (ascPochhammer R n).eval ((n : R) + α + β + 1) := by
  rw [leadingCoeff, natDegree_eq_of_degree_eq_some (degree_jacobi_eq α β n h),
    coeff_jacobi_self]

Theorem 3.2.3 Jacobi value at one

✓ 🙂 human-reviewed

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\alpha ,\beta \in R\), and let \(n\in \mathbb {N}\). Then \(P_n^{(\alpha ,\beta )}(1)=(\alpha +1)_n/n!\). In particular, \((n+1)P_{n+1}^{(\alpha ,\beta )}(1)=(n+\alpha +1)P_n^{(\alpha ,\beta )}(1)\).

Reference: [DLMF, Table 18.6.1].

Lean Formalisation

theorem Polynomial.eval_jacobi_one.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ) :
  Polynomial.eval 1 (Polynomial.jacobi α β n) =
    (algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval (α + 1) (ascPochhammer R n)

Lean proof

/-- The endpoint normalisation (DLMF Table 18.6.1). -/
@[simp] theorem eval_jacobi_one (α β : R) (n : ℕ) :
    (jacobi α β n).eval 1 = algebraMap ℚ R ((n.factorial : ℚ)⁻¹) *
      (ascPochhammer R n).eval (α + 1) := by
  unfold jacobi
  rw [eval_finsetSum, Finset.sum_eq_single 0]
  · simp
  · intro l hl hl0
    simp [hl0]
  · simp

1 related Lean declaration

theorem Polynomial.succ_mul_eval_jacobi_one.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ) :
  (↑n + 1) * Polynomial.eval 1 (Polynomial.jacobi α β (n + 1)) =
    (↑n + α + 1) * Polynomial.eval 1 (Polynomial.jacobi α β n)

Lean proof

/-- Successive endpoint values satisfy a cleared rising-factorial relation
(DLMF Table 18.6.1). -/
theorem succ_mul_eval_jacobi_one {R : Type*} [CommRing R] [Algebra ℚ R]
    (α β : R) (n : ℕ) :
    (n + 1 : R) * (jacobi α β (n + 1)).eval 1 =
      (n + α + 1) * (jacobi α β n).eval 1 := by
  rw [eval_jacobi_one, eval_jacobi_one, ascPochhammer_succ_eval]
  have hf : (n + 1 : R) * algebraMap ℚ R (((n + 1).factorial : ℚ)⁻¹) =
      algebraMap ℚ R ((n.factorial : ℚ)⁻¹) :=
    Nat.cast_succ_mul_algebraMap_inv_factorial R n
  linear_combination (ascPochhammer R n).eval (α + 1) * (α + 1 + n) * hf

Theorem 3.2.4 Special values and symmetry

✓ 🙂 human-reviewed

#

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

\[ P_n^{(\alpha ,\beta )}(-X)=(-1)^nP_n^{(\beta ,\alpha )}(X),\qquad P_n^{(\alpha ,\beta )}(-1)=(-1)^n\frac{(\beta +1)_n}{n!}. \]

Reference: [DLMF, Table 18.6.1].

Lean Formalisation

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

Lean proof

/-- Reflection swaps the Jacobi parameters, including degenerate specialisations
(DLMF Table 18.6.1). -/
theorem jacobi_comp_neg_X {R : Type*} [CommRing R] [Algebra ℚ R]
    (α β : R) (n : ℕ) :
    (jacobi α β n).comp (-X) = C ((-1 : R) ^ n) * jacobi β α n := by
  have h := jacobi_comp_neg_X_of_nonzero (X : ℚ[X][X]) (C X) n (fun k hk ↦ by
    have hc := congrArg (fun p : ℚ[X][X] ↦ p.coeff 1) hk
    have hk : (k : ℚ[X][X]) = C (k : ℚ[X]) := by simp
    rw [hk] at hc
    norm_num [coeff_add, coeff_one] at hc)
  let f : ℚ[X][X] →ₐ[ℚ] R := eval₂AlgHom (aeval β) α (fun _ ↦ Commute.all _ _)
  have hm := congrArg (Polynomial.map f.toRingHom) h
  simp only [map_comp, Polynomial.map_neg, map_X, Polynomial.map_mul,
    Polynomial.map_C, map_jacobi] at hm
  simpa [f, eval₂_pow, eval₂_neg, eval₂_one] using hm

2 related Lean declarations

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

Lean proof

/-- Evaluation form of Jacobi reflection (DLMF Table 18.6.1). -/
theorem eval_jacobi_neg {R : Type*} [CommRing R] [Algebra ℚ R]
    (α β x : R) (n : ℕ) :
    (jacobi α β n).eval (-x) = (-1 : R) ^ n * (jacobi β α n).eval x := by
  have h := congrArg (fun p : R[X] ↦ p.eval x) (jacobi_comp_neg_X α β n)
  simpa only [eval_comp, eval_neg, eval_X, eval_mul, eval_C] using h

theorem Polynomial.eval_jacobi_neg_one.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ) :
  Polynomial.eval (-1) (Polynomial.jacobi α β n) =
    (-1) ^ n * ((algebraMap ℚ R) (↑n.factorial)⁻¹ * Polynomial.eval (β + 1) (ascPochhammer R n))

Lean proof

/-- The other endpoint normalisation (DLMF Table 18.6.1). -/
theorem eval_jacobi_neg_one {R : Type*} [CommRing R] [Algebra ℚ R]
    (α β : R) (n : ℕ) :
    (jacobi α β n).eval (-1) = (-1 : R) ^ n *
      (algebraMap ℚ R ((n.factorial : ℚ)⁻¹) * (ascPochhammer R n).eval (β + 1)) := by
  rw [eval_jacobi_neg, eval_jacobi_one]

Parameter substitution and low degrees

Theorem 3.2.5 Low degrees and parameter substitution

✓ 🙂 human-reviewed

#

For a commutative \(\mathbb {Q}\)-algebra \(R\) and \(\alpha ,\beta \in R\),

\[ P_0^{(\alpha ,\beta )}=1,\qquad P_1^{(\alpha ,\beta )}=(\alpha +1)+\tfrac 12(\alpha +\beta +2)(X-1). \]

For every \(\mathbb {Q}\)-algebra homomorphism \(f:R\to S\) and \(n\in \mathbb {N}\), applying \(f\) to the coefficients of \(P_n^{(\alpha ,\beta )}\) gives \(P_n^{(f(\alpha ),f(\beta ))}\).

Reference: [DLMF, 18.5.7].

Lean Formalisation

theorem Polynomial.jacobi_zero.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) : Polynomial.jacobi α β 0 = 1

Lean proof

/-- The constant member is one (DLMF 18.5.7). -/
@[simp] theorem jacobi_zero (α β : R) : jacobi α β 0 = 1 := by
  simp [jacobi]

2 related Lean declarations

theorem Polynomial.jacobi_one.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) :
  Polynomial.jacobi α β 1 =
    Polynomial.C (α + 1) + Polynomial.C ((algebraMap ℚ R) (1 / 2) * (α + β + 2)) * (Polynomial.X - 1)

Lean proof

/-- The first member, valid even when its leading coefficient vanishes
(DLMF 18.5.7). -/
theorem jacobi_one (α β : R) :
    jacobi α β 1 = C (α + 1) +
      C (algebraMap ℚ R (1 / 2) * (α + β + 2)) * (X - 1) := by
  simp only [one_div, jacobi, Finset.sum_range_succ, Finset.sum_range_zero, zero_add,
    Nat.factorial_zero, Nat.factorial_one, Nat.sub_zero, Nat.sub_self,
    Nat.cast_zero, Nat.cast_one, pow_zero, pow_one, one_mul, mul_one,
    inv_one, map_one, ascPochhammer_zero, ascPochhammer_one, eval_one, eval_X,
    add_zero]
  congr 2
  ring_nf

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

Lean proof

/-- Jacobi polynomials commute with rational algebra maps (DLMF 18.5.7). -/
theorem map_jacobi (f : R →ₐ[ℚ] S) (α β : R) (n : ℕ) :
    (jacobi α β n).map f.toRingHom = jacobi (f α) (f β) 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 [jacobi, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C,
    Polynomial.map_pow, Polynomial.map_sub, map_X, Polynomial.map_one,
    AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, map_mul, hp, map_add, map_natCast, map_one, AlgHom.commutes]

3.2.2 Polynomial and weighted identities

The derivative shifts both parameters. The recurrence, differential equation, Rodrigues formula and terminating Gauss series give complementary descriptions of the same polynomials.

Theorem 3.2.6 Jacobi derivative

✓ 🙂 human-reviewed

#

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

\[ (P_{n+1}^{(\alpha ,\beta )})'=\tfrac 12(n+\alpha +\beta +2) P_n^{(\alpha +1,\beta +1)}. \]

Reference: [DLMF, 18.9.15].

Lean Formalisation

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

Lean proof

/-- Differentiation raises both Jacobi parameters by one (DLMF 18.9.15). -/
theorem derivative_jacobi_succ (α β : R) (n : ℕ) :
    derivative (jacobi α β (n + 1)) =
      C (algebraMap ℚ R (1 / 2) * ((n : R) + α + β + 2)) *
        jacobi (α + 1) (β + 1) n := by
  let c (α β : R) (n l : ℕ) : R :=
    algebraMap ℚ R (((l.factorial : ℚ) * (n - l).factorial * 2 ^ l)⁻¹) *
      (ascPochhammer R l).eval ((n : R) + α + β + 1) *
      (ascPochhammer R (n - l)).eval (α + l + 1)
  have hrat (l : ℕ) :
      (l + 1 : ℚ) * (((l + 1).factorial : ℚ) * (n - l).factorial * 2 ^ (l + 1))⁻¹ =
      (1 / 2 : ℚ) * (((l.factorial : ℚ) * (n - l).factorial * 2 ^ l)⁻¹) := by
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, pow_succ]
    field_simp
  have hc (l : ℕ) : c α β (n + 1) (l + 1) * (l + 1 : R) =
      (algebraMap ℚ R (1 / 2) * ((n : R) + α + β + 2)) *
        c (α + 1) (β + 1) n l := by
    have hm := congrArg (algebraMap ℚ R) (hrat l)
    simp only [map_mul, map_add, map_natCast, map_one] at hm
    dsimp only [c]
    rw [Nat.add_sub_add_right, ascPochhammer_succ_left, eval_mul, eval_X,
      eval_comp, eval_add, eval_X, eval_one]
    simp only [Nat.cast_add, Nat.cast_one]
    have h1 : (n : R) + 1 + α + β + 1 = n + α + β + 2 := by ring
    have h2 : (n : R) + α + β + 2 + 1 = n + (α + 1) + (β + 1) + 1 := by ring
    have h3 : α + ((l : R) + 1) + 1 = (α + 1) + l + 1 := by ring
    rw [h1, h2, h3]
    calc
      _ = ((l + 1 : R) * algebraMap ℚ R
          ((( (l + 1).factorial : ℚ) * (n - l).factorial * 2 ^ (l + 1))⁻¹)) *
          ((n : R) + α + β + 2) *
          (ascPochhammer R l).eval ((n : R) + (α + 1) + (β + 1) + 1) *
          (ascPochhammer R (n - l)).eval ((α + 1) + l + 1) := by ring
      _ = _ := by rw [hm]; ring
  change derivative (∑ l ∈ Finset.range (n + 1 + 1), C (c α β (n + 1) l) *
    (X - 1) ^ l) = C _ * ∑ l ∈ Finset.range (n + 1),
      C (c (α + 1) (β + 1) n l) * (X - 1) ^ l
  rw [derivative_sum, Finset.sum_range_succ']
  simp only [pow_zero, mul_one, derivative_C, add_zero, Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro l _
  rw [derivative_C_mul, derivative_pow_succ, derivative_sub, derivative_X,
    derivative_one, sub_zero, mul_one, ← mul_assoc, ← C_mul, hc, C_mul, mul_assoc]

Theorem 3.2.7 Cleared Jacobi recurrence

✓ 🤖

#

Let \(R\) be a commutative \(\mathbb {Q}\)-algebra, let \(\alpha ,\beta \in R\), and let \(n\in \mathbb {N}\). Put \(s=\alpha +\beta \). Then

\begin{align*} & 2(n+2)(n+s+2)(2n+s+2)P_{n+2}^{(\alpha ,\beta )}\\ & \quad =(2n+s+3)\bigl[(2n+s+2)(2n+s+4)X+\alpha ^2-\beta ^2\bigr] P_{n+1}^{(\alpha ,\beta )}\\ & \qquad \quad -2(n+\alpha +1)(n+\beta +1)(2n+s+4)P_n^{(\alpha ,\beta )}. \end{align*}

No factor depending on parameters is inverted, including at degenerate specialisations.

Reference: [DLMF, 18.9.1–18.9.2].

Lean Formalisation

theorem Polynomial.jacobi_recurrence.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ) :
  Polynomial.C (2 * (↑n + 2) * (↑n + α + β + 2) * (2 * ↑n + α + β + 2)) * Polynomial.jacobi α β (n + 2) =
    Polynomial.C (2 * ↑n + α + β + 3) *
          (Polynomial.C ((2 * ↑n + α + β + 2) * (2 * ↑n + α + β + 4)) * Polynomial.X + Polynomial.C (α ^ 2 - β ^ 2)) *
        Polynomial.jacobi α β (n + 1) -
      Polynomial.C (2 * (↑n + α + 1) * (↑n + β + 1) * (2 * ↑n + α + β + 4)) * Polynomial.jacobi α β n

Lean proof

/-- The three-term Jacobi recurrence with all parameter denominators cleared,
valid over every commutative rational algebra (DLMF 18.9.1--2, index shifted by one). -/
theorem jacobi_recurrence {R : Type*} [CommRing R] [Algebra ℚ R]
    (α β : R) (n : ℕ) :
    C (2 * (n + 2) * (n + α + β + 2) * (2 * n + α + β + 2)) * jacobi α β (n + 2) =
      C (2 * n + α + β + 3) *
        (C ((2 * n + α + β + 2) * (2 * n + α + β + 4)) * X + C (α ^ 2 - β ^ 2)) *
        jacobi α β (n + 1) -
      C (2 * (n + α + 1) * (n + β + 1) * (2 * n + α + β + 4)) * jacobi α β n := by
  have h := jacobi_recurrence_of_nonzero (X : ℚ[X][X]) (C X) n (fun k hk ↦ by
    have hc := congrArg (fun p : ℚ[X][X] ↦ p.coeff 1) hk
    norm_num [coeff_add, coeff_natCast_ite, coeff_one] at hc)
  let f : ℚ[X][X] →ₐ[ℚ] R := eval₂AlgHom (aeval β) α (fun _ ↦ Commute.all _ _)
  have hm := congrArg (Polynomial.map f.toRingHom) h
  simp only [Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_add,
    Polynomial.map_C, map_X, map_jacobi] at hm
  simpa [f, eval₂_add, eval₂_sub, eval₂_mul, eval₂_pow, eval₂_natCast, eval₂_ofNat] using hm

Theorem 3.2.8 Jacobi differential equation

✓ 🙂 human-reviewed

#

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

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

Reference: [DLMF, Table 18.8.1].

Lean Formalisation

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

Lean proof

/-- The Jacobi differential equation, without parameter restrictions
(DLMF Table 18.8.1). -/
theorem jacobi_differentialEquation (α β : R) (n : ℕ) :
    (1 - X ^ 2) * derivative (derivative (jacobi α β n)) +
      (C (β - α) - C (α + β + 2) * X) * derivative (jacobi α β n) +
      C ((n : R) * ((n : R) + α + β + 1)) * jacobi α β n = 0 := by
  let : HasUniqueDiv R := HasUniqueDiv.of_module_rat R
  induction n generalizing α β with
  | zero => simp
  | succ n ih =>
    let p := jacobi α β (n + 1)
    let q := jacobi (α + 1) (β + 1) n
    let d := algebraMap ℚ R (1 / 2) * ((n : R) + α + β + 2)
    let r := (1 - X ^ 2) * derivative (derivative p) +
      (C (β - α) - C (α + β + 2) * X) * derivative p +
      C (((n + 1 : ℕ) : R) * (((n + 1 : ℕ) : R) + α + β + 1)) * p
    have hp : derivative p = C d * q := derivative_jacobi_succ α β n
    have hr : derivative r = 0 := by
      dsimp only [r]
      simp only [derivative_add, derivative_mul, derivative_sub, derivative_one,
        derivative_X_pow, derivative_X, derivative_C, zero_mul, zero_sub,
        zero_add, mul_one]
      rw [hp, derivative_C_mul, derivative_C_mul]
      have hi := ih (α + 1) (β + 1)
      change (1 - X ^ 2) * derivative (derivative q) +
        (C ((β + 1) - (α + 1)) - C ((α + 1) + (β + 1) + 2) * X) * derivative q +
        C ((n : R) * ((n : R) + (α + 1) + (β + 1) + 1)) * q = 0 at hi
      simp only [Nat.cast_add, Nat.cast_one, map_add, map_sub, map_mul,
        map_natCast, map_ofNat, map_one] at hi ⊢
      linear_combination C d * hi
    have hhalf : (2 : R) * algebraMap ℚ R (1 / 2) = 1 := by
      have h := congrArg (algebraMap ℚ R) (show (2 : ℚ) * (1 / 2) = 1 by norm_num)
      simpa only [map_mul, map_ofNat, map_one] using h
    have hfact : (n + 1 : R) * algebraMap ℚ R (((n + 1).factorial : ℚ)⁻¹) =
        algebraMap ℚ R ((n.factorial : ℚ)⁻¹) :=
      Nat.cast_succ_mul_algebraMap_inv_factorial R n
    have heval : r.eval 1 = 0 := by
      dsimp only [r]
      simp only [eval_add, eval_mul, eval_sub, eval_one, eval_pow, eval_X,
        one_pow, sub_self, zero_mul, zero_add, eval_C, mul_one]
      rw [hp, eval_mul, eval_C]
      dsimp only [p, q, d]
      rw [eval_jacobi_one, eval_jacobi_one, ascPochhammer_succ_left,
        eval_mul, eval_X, eval_comp, eval_add, eval_X, eval_one]
      simp only [Nat.cast_add, Nat.cast_one]
      have harg : (n : R) + 1 + α + β + 1 = n + α + β + 2 := by ring
      rw [harg]
      calc
        _ = (-(2 * algebraMap ℚ R (1 / 2)) * algebraMap ℚ R ((n.factorial : ℚ)⁻¹) +
            (n + 1 : R) * algebraMap ℚ R (((n + 1).factorial : ℚ)⁻¹)) *
            ((n : R) + α + β + 2) * (α + 1) *
            (ascPochhammer R n).eval (α + 1 + 1) := by ring
        _ = 0 := by rw [hhalf, hfact]; ring
    have hconst := eq_C_of_derivative_eq_zero hr
    have hc := congrArg (fun p : R[X] => p.eval 1) hconst
    simp only [eval_C] at hc
    have hcoeff : r.coeff 0 = 0 := hc.symm.trans heval
    change r = 0
    rw [hconst, hcoeff, C_0]

Definition 3.2.9 Jacobi weight and measure

✓ 🙂 human-reviewed

#

For real \(\alpha ,\beta \), define the continuous map \(w_{\alpha ,\beta }:(-1,1)\to \mathbb {R}_{\ge 0}\) by \(w_{\alpha ,\beta }(x)=(1-x)^\alpha (1+x)^\beta \). Let \(\mu _{\alpha ,\beta }=\mu _{w_{\alpha ,\beta }}\) be the measure of Definition 1.1.2 for this weight on \((-1,1)\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

def Polynomial.jacobiWeight (α β : ℝ) : C(↑(Set.Ioo (-1) 1), NNReal)

Lean definition

/-- The Jacobi weight on its open interval, with nonnegative values. -/
noncomputable def jacobiWeight (α β : ℝ) : C(Ioo (-1 : ℝ) 1, ℝ≥0) where
  toFun x := ⟨(1 - (x : ℝ)) ^ α * (1 + (x : ℝ)) ^ β,
    mul_nonneg (Real.rpow_nonneg (by linarith [x.property.2]) _)
      (Real.rpow_nonneg (by linarith [x.property.1]) _)⟩
  continuous_toFun := by
    apply Continuous.subtype_mk
    apply Continuous.mul
    · exact (continuous_const.sub continuous_subtype_val).rpow_const
        (fun x ↦ Or.inl (by change 1 - (x : ℝ) ≠ 0; linarith [x.property.2]))
    · exact (continuous_const.add continuous_subtype_val).rpow_const
        (fun x ↦ Or.inl (by change 1 + (x : ℝ) ≠ 0; linarith [x.property.1]))

1 related Lean declaration

def Polynomial.jacobiMeasure (α β : ℝ) : MeasureTheory.Measure ℝ

Lean definition

/-- The classical Jacobi measure: subtype density followed by inclusion. -/
noncomputable def jacobiMeasure (α β : ℝ) : Measure ℝ :=
  openIntervalWeightMeasure (-1) 1 (jacobiWeight α β)

Theorem 3.2.10 Jacobi integral characterisation

✓ 🙂 human-reviewed

#

A real function \(f\) is \(\mu _{\alpha ,\beta }\)-integrable if and only if \(x\mapsto w_{\alpha ,\beta }(x)f(x)\) is Lebesgue-integrable on \((-1,1)\). When these equivalent integrability conditions hold,

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

Lean Formalisation

theorem Polynomial.integrable_jacobiMeasure_iff (α β : ℝ) (f : ℝ → ℝ) :
  MeasureTheory.Integrable f (Polynomial.jacobiMeasure α β) ↔
    MeasureTheory.Integrable (fun x => ↑((Polynomial.jacobiWeight α β) x) * f ↑x) MeasureTheory.volume

Lean proof

/-- Characterization of integrability against the classical Jacobi measure. -/
theorem integrable_jacobiMeasure_iff (α β : ℝ) (f : ℝ → ℝ) :
    Integrable f (jacobiMeasure α β) ↔
      Integrable (fun x : Ioo (-1 : ℝ) 1 ↦ (jacobiWeight α β x : ℝ) * f x) volume :=
  integrable_openIntervalWeightMeasure_iff _ _ _ _

1 related Lean declaration

theorem Polynomial.integral_jacobiMeasure (α β : ℝ) (f : MeasureTheory.IntegrableInput (Polynomial.jacobiMeasure α β)) :
  ∫ (x : ℝ), ↑f x ∂Polynomial.jacobiMeasure α β = ∫ (x : ↑(Set.Ioo (-1) 1)), ↑((Polynomial.jacobiWeight α β) x) * ↑f ↑x

Lean proof

/-- Characterization of its integral for a bundled integrable input. -/
theorem integral_jacobiMeasure (α β : ℝ)
    (f : IntegrableInput (jacobiMeasure α β)) :
    ∫ x, f.val x ∂jacobiMeasure α β =
      ∫ x : Ioo (-1 : ℝ) 1, (jacobiWeight α β x : ℝ) * f.val x :=
  integral_openIntervalWeightMeasure _ _ _ _

Theorem 3.2.11 Weighted Jacobi Rodrigues formula

✓ 🤖

#

For all real \(\alpha ,\beta \), \(n\ge 0\), and \(-1{\lt}x{\lt}1\), write \(w_{\alpha ,\beta }(x)=(1-x)^\alpha (1+x)^\beta \). Then

\[ \frac{d}{dx}\left(w_{\alpha +1,\beta +1}(x)P_n^{(\alpha +1,\beta +1)}(x)\right) =-2(n+1)w_{\alpha ,\beta }(x)P_{n+1}^{(\alpha ,\beta )}(x), \]

\[ \frac{d^n}{dx^n}w_{\alpha +n,\beta +n}(x) =(-2)^n n!\, w_{\alpha ,\beta }(x)P_n^{(\alpha ,\beta )}(x). \]

The weight is strictly positive in the open interval, so division gives the usual Rodrigues representation. No integrability or endpoint regularity hypothesis is imposed.

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

Lean Formalisation

theorem Polynomial.hasDerivAt_jacobiWeight_mul_jacobi (α β : ℝ) (n : ℕ) (x : ↑(Set.Ioo (-1) 1)) :
  HasDerivAtOnOpen { carrier := Set.Ioo (-1) 1, is_open' := ⋯ }
    (fun y =>
      ↑((Polynomial.jacobiWeight (α + 1) (β + 1)) y) * Polynomial.eval (↑y) (Polynomial.jacobi (α + 1) (β + 1) n))
    (-2 * (↑n + 1) * ↑((Polynomial.jacobiWeight α β) x) * Polynomial.eval (↑x) (Polynomial.jacobi α β (n + 1))) x

Lean proof

/-- The weighted lowering identity is a genuine derivative on the open domain
(DLMF 18.9.16). -/
theorem hasDerivAt_jacobiWeight_mul_jacobi (α β : ℝ) (n : ℕ)
    (x : Ioo (-1 : ℝ) 1) :
    HasDerivAtOnOpen ⟨Ioo (-1 : ℝ) 1, isOpen_Ioo⟩
      (fun y ↦ (jacobiWeight (α + 1) (β + 1) y : ℝ) *
        (jacobi (α + 1) (β + 1) n).eval (y : ℝ))
      (-2 * (n + 1 : ℝ) * (jacobiWeight α β x : ℝ) *
        (jacobi α β (n + 1)).eval (x : ℝ)) x := by
  have hP : HasDerivAtOnOpen ⟨Ioo (-1 : ℝ) 1, isOpen_Ioo⟩
      (fun y ↦ (jacobi (α + 1) (β + 1) n).eval (y : ℝ))
      ((jacobi (α + 1) (β + 1) n).derivative.eval (x : ℝ)) x :=
    ⟨fun t ↦ (jacobi (α + 1) (β + 1) n).eval t, fun _ ↦ rfl,
      (jacobi (α + 1) (β + 1) n).hasDerivAt x⟩
  have hd := (hasDerivAt_jacobiWeight_add_one α β x).mul hP
  have he := congrArg (fun p : ℝ[X] ↦ p.eval (x : ℝ)) (jacobi_rodrigues_step α β n)
  simp only [eval_add, eval_sub, eval_mul, eval_pow, eval_one, eval_X, eval_C, eval_neg] at he
  convert hd using 1
  rw [jacobiWeight_add_one α β x]
  linear_combination -(jacobiWeight α β x : ℝ) * he

2 related Lean declarations

theorem Polynomial.hasIteratedDeriv_jacobiWeight (α β : ℝ) (n : ℕ) :
  HasIteratedDerivOnOpen { carrier := Set.Ioo (-1) 1, is_open' := ⋯ } n
    (fun x => ↑((Polynomial.jacobiWeight (α + ↑n) (β + ↑n)) x)) fun x =>
    (-2) ^ n * ↑n.factorial * ↑((Polynomial.jacobiWeight α β) x) * Polynomial.eval (↑x) (Polynomial.jacobi α β n)

Lean proof

/-- Rodrigues' formula with an actual chain of derivatives, for every real
parameter pair (DLMF 18.5.5). No endpoint regularity is required. -/
theorem hasIteratedDeriv_jacobiWeight (α β : ℝ) (n : ℕ) :
    HasIteratedDerivOnOpen ⟨Ioo (-1 : ℝ) 1, isOpen_Ioo⟩ n
      (fun x ↦ (jacobiWeight (α + n) (β + n) x : ℝ))
      (fun x ↦ (-2 : ℝ)^n * n.factorial * (jacobiWeight α β x : ℝ) *
        (jacobi α β n).eval (x : ℝ)) := by
  induction n generalizing α β with
  | zero =>
    change (fun x ↦ (jacobiWeight (α + (0 : ℕ)) (β + (0 : ℕ)) x : ℝ)) = _
    funext x
    simp
  | succ n ih =>
    refine ⟨fun x ↦ (-2 : ℝ)^n * n.factorial *
      (jacobiWeight (α+1) (β+1) x : ℝ) * (jacobi (α+1) (β+1) n).eval (x : ℝ), ?_, ?_⟩
    · have ha : α + ((n+1 : ℕ) : ℝ) = (α+1) + n := by push_cast; ring
      have hb : β + ((n+1 : ℕ) : ℝ) = (β+1) + n := by push_cast; ring
      simpa only [ha, hb] using ih (α+1) (β+1)
    · intro x
      have hd := (hasDerivAt_jacobiWeight_mul_jacobi α β n x).const_mul
        ((-2 : ℝ)^n * n.factorial)
      convert hd using 1
      · funext y
        ring
      · rw [pow_succ, Nat.factorial_succ]
        push_cast
        ring

theorem Polynomial.eval_jacobi_eq_rodrigues (α β : ℝ) (n : ℕ) :
  ∃ d,
    HasIteratedDerivOnOpen { carrier := Set.Ioo (-1) 1, is_open' := ⋯ } n
        (fun x => ↑((Polynomial.jacobiWeight (α + ↑n) (β + ↑n)) x)) d ∧
      ∀ (x : ↑(Set.Ioo (-1) 1)),
        Polynomial.eval (↑x) (Polynomial.jacobi α β n) =
          d x / ((-2) ^ n * ↑n.factorial * ↑((Polynomial.jacobiWeight α β) x))

Lean proof

/-- The divided Rodrigues representation includes existence of its numerator
as an iterated derivative (DLMF 18.5.5). -/
theorem eval_jacobi_eq_rodrigues (α β : ℝ) (n : ℕ) :
    ∃ d : Ioo (-1 : ℝ) 1 → ℝ,
      HasIteratedDerivOnOpen ⟨Ioo (-1 : ℝ) 1, isOpen_Ioo⟩ n
        (fun x ↦ (jacobiWeight (α+n) (β+n) x : ℝ)) d ∧
      ∀ x : Ioo (-1 : ℝ) 1, (jacobi α β n).eval (x : ℝ) =
        d x / ((-2 : ℝ)^n * n.factorial * (jacobiWeight α β x : ℝ)) := by
  refine ⟨_, hasIteratedDeriv_jacobiWeight α β n, ?_⟩
  intro x
  have hd : (-2 : ℝ)^n * n.factorial * (jacobiWeight α β x : ℝ) ≠ 0 :=
    mul_ne_zero (mul_ne_zero (pow_ne_zero _ (by norm_num))
      (Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n))) (jacobiWeight_pos α β x).ne'
  exact (mul_div_cancel_left₀ _ hd).symm

Theorem 3.2.12 Jacobi hypergeometric representation

✓ 🤖

#

Let \(R\) be a characteristic-zero field with a rational algebra structure, let \(\alpha ,\beta ,x\in R\), and let \(n\in \mathbb {N}\). Assume \((\alpha +1)_n\ne 0\). Then

\[ P_n^{(\alpha ,\beta )}(x)=\frac{(\alpha +1)_n}{n!} \sum _{k=0}^n\frac{(-n)_k(n+\alpha +\beta +1)_k}{(\alpha +1)_k k!} \left(\frac{1-x}{2}\right)^k. \]

For real or complex scalars this equals

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

where \({}_2F_1\) is the Gauss series of Definition 1.2.6. The finite nonvanishing condition excludes zeros among exactly the denominator factors needed through degree \(n\); \(x\) is unrestricted.

Reference: [DLMF, 18.5.7].

Lean Formalisation

theorem Polynomial.eval_jacobi_eq_hypergeometric_sum.{u_1} {R : Type u_1} [Field R] [CharZero R] [Algebra ℚ R] (α β x : R)
  (n : ℕ) (hc : Polynomial.eval (α + 1) (ascPochhammer R n) ≠ 0) :
  Polynomial.eval x (Polynomial.jacobi α β n) =
    Polynomial.eval (α + 1) (ascPochhammer R n) / ↑n.factorial *
      ∑ k ∈ Finset.range (n + 1),
        ordinaryHypergeometricCoefficientOn (GaussParameters.ofTerminating (-↑n) (↑n + α + β + 1) (α + 1) n ⋯ hc) k *
          ((1 - x) / 2) ^ k

Lean proof

/-- The finite Jacobi representation with only certified classical coefficients. -/
theorem eval_jacobi_eq_hypergeometric_sum {R : Type*} [Field R] [CharZero R]
    [Algebra ℚ R] (α β x : R) (n : ℕ)
    (hc : (ascPochhammer R n).eval (α + 1) ≠ 0) :
    (jacobi α β n).eval x = (ascPochhammer R n).eval (α + 1) / n.factorial *
      ∑ k ∈ Finset.range (n + 1),
        ordinaryHypergeometricCoefficientOn
          (GaussParameters.ofTerminating (-(n : R)) (n + α + β + 1) (α + 1) n (Or.inl rfl) hc) k *
          ((1 - x) / 2) ^ k := by
  rw [jacobi, eval_finsetSum, Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro k hk
  have hkn : k ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hk)
  have hck := GaussParameters.pochhammer_ne_zero_of_le (α + 1) hc hkn
  rw [ordinaryHypergeometricCoefficientOn_eq_div _ k hck]
  simp only [eval_mul, eval_C, eval_pow, eval_sub, eval_X, eval_one,
    GaussParameters.ofTerminating]
  simpa only [ordinaryHypergeometricCoefficient, div_eq_mul_inv, mul_inv_rev,
    mul_assoc, mul_left_comm, mul_comm] using
    jacobi_hypergeometric_term α β x n k hkn hc

1 related Lean declaration

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

Lean proof

/-- Jacobi's terminating classical Gauss representation with its original finite admissibility. -/
theorem eval_jacobi_eq_ordinaryHypergeometric {𝕂 : Type*} [RCLike 𝕂]
    (α β x : 𝕂) (n : ℕ) (hc : (ascPochhammer 𝕂 n).eval (α + 1) ≠ 0) :
    (jacobi α β n).eval x = (ascPochhammer 𝕂 n).eval (α + 1) / n.factorial *
      ordinaryHypergeometricOn (GaussParameters.ofTerminating (-(n : 𝕂)) (n + α + β + 1) (α + 1) n (Or.inl rfl) hc)
        (.ofTerminating _ n (Or.inl rfl) ((1 - x) / 2)) := by
  rw [ordinaryHypergeometricOn_terminating]
  exact eval_jacobi_eq_hypergeometric_sum α β x n hc

Rodrigues proofs, Beta and Euler integrals

Theorem 3.2.13 Jacobi density characterisation

✓ 🙂 human-reviewed

#

For every \(x\in (-1,1)\), \(w_{\alpha ,\beta }(x)=(1-x)^\alpha (1+x)^\beta \).

Lean Formalisation

theorem Polynomial.jacobiWeight_apply (α β : ℝ) (x : ↑(Set.Ioo (-1) 1)) :
  ↑((Polynomial.jacobiWeight α β) x) = (1 - ↑x) ^ α * (1 + ↑x) ^ β

Lean proof

/-- The defining weight formula only has strictly positive power bases. -/
theorem jacobiWeight_apply (α β : ℝ) (x : Ioo (-1 : ℝ) 1) :
    (jacobiWeight α β x : ℝ) = (1 - (x : ℝ)) ^ α * (1 + (x : ℝ)) ^ β := rfl

Theorem 3.2.14 Algebraic Jacobi Rodrigues step

✓ 🤖

#

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

\[ (1-X^2)Q'+[\beta -\alpha -(\alpha +\beta +2)X]Q =-2(n+1)P_{n+1}^{(\alpha ,\beta )}. \]

No parameter factor is cancelled in the final identity.

Reference: [DLMF, 18.5.5 and 18.9.16].

Lean Formalisation

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

Lean proof

/-- The polynomial first-order identity underlying Jacobi Rodrigues' formula,
with no parameter restrictions (DLMF 18.5.5 and 18.9.16). -/
theorem jacobi_rodrigues_step {R : Type*} [CommRing R] [Algebra ℚ R]
    (α β : R) (n : ℕ) :
    (1 - X ^ 2) * derivative (jacobi (α + 1) (β + 1) n) +
      (C (β - α) - C (α + β + 2) * X) * jacobi (α + 1) (β + 1) n =
      -C (2 * (n + 1 : R)) * jacobi α β (n + 1) := by
  have h := jacobi_rodrigues_step_of_ne_zero (X : ℚ[X][X]) (C X) n (by
    intro hz
    have hc := congrArg (fun p : ℚ[X][X] ↦ p.coeff 1) hz
    norm_num [coeff_add, coeff_natCast_ite] at hc)
  let f : ℚ[X][X] →ₐ[ℚ] R := eval₂AlgHom (aeval β) α (fun _ ↦ Commute.all _ _)
  have hm := congrArg (Polynomial.map f.toRingHom) h
  simp only [Polynomial.map_add, Polynomial.map_sub, Polynomial.map_mul,
    Polynomial.map_neg, Polynomial.map_pow, Polynomial.map_one, Polynomial.map_C,
    map_X, ← derivative_map, map_jacobi] at hm
  simpa [f, eval₂_add, eval₂_sub, eval₂_mul, eval₂_natCast, eval₂_ofNat] using hm

Theorem 3.2.15 Uniqueness at the Jacobi endpoint

✓ 🤖

#

Let \(R\) be a characteristic-zero commutative domain and a \(\mathbb {Q}\)-algebra. Suppose \(\alpha +k+1\ne 0\) for every \(k\in \mathbb {N}\). For any \(\beta ,\gamma \in R\), a polynomial \(p\) satisfying

\[ (1-X^2)p''+[\beta -\alpha -(\alpha +\beta +2)X]p'+\gamma p=0,\qquad p(1)=0 \]

is zero.

Reference: [DLMF, Table 18.8.1].

Lean Formalisation

theorem Polynomial.eq_zero_of_jacobi_ode.{u_1} {R : Type u_1} [CommRing R] [IsDomain R] [CharZero R] [Algebra ℚ R] (α β γ : R)
  (p : Polynomial R) (hα : ∀ (k : ℕ), α + ↑k + 1 ≠ 0)
  (he :
    (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.derivative p) +
          (Polynomial.C (β - α) - Polynomial.C (α + β + 2) * Polynomial.X) * Polynomial.derivative p +
        Polynomial.C γ * p =
      0)
  (hv : Polynomial.eval 1 p = 0) : p = 0

Lean proof

/-- A polynomial solution vanishing at one is zero when the endpoint coefficients
are nonzero (DLMF Table 18.8.1). -/
theorem eq_zero_of_jacobi_ode {R : Type*} [CommRing R] [IsDomain R] [CharZero R] [Algebra ℚ R]
    (α β γ : R) (p : R[X])
    (hα : ∀ k : ℕ, α + k + 1 ≠ 0)
    (he : (1 - X ^ 2) * derivative (derivative p) +
      (C (β - α) - C (α + β + 2) * X) * derivative p + C γ * p = 0)
    (hv : p.eval 1 = 0) : p = 0 := by
  let : HasUniqueDiv R := HasUniqueDiv.of_module_rat R
  induction hn : p.natDegree using Nat.strong_induction_on generalizing α β γ p with
  | h n ih =>
    have hdv : (derivative p).eval 1 = 0 := by
      have h := congrArg (fun q : R[X] ↦ q.eval 1) he
      simp only [eval_add, eval_mul, eval_sub, eval_one, eval_pow, eval_X,
        one_pow, sub_self, zero_mul, zero_add, eval_C, eval_zero, mul_one, hv, mul_zero, add_zero] at h
      have hz : (-2 * (α + 1)) * (derivative p).eval 1 = 0 := by
        linear_combination h
      exact (mul_eq_zero.mp hz).resolve_left (mul_ne_zero (by norm_num) (by simpa using hα 0))
    have hd : derivative p = 0 := by
      by_cases hp : p.natDegree = 0
      · exact derivative_of_natDegree_zero hp
      have he' := congrArg derivative he
      simp only [derivative_add, derivative_mul, derivative_sub, derivative_one,
        derivative_X_pow, Nat.cast_ofNat, Nat.reduceSub, pow_one, derivative_X, derivative_C, zero_mul, zero_sub,
        zero_add, mul_one, derivative_zero] at he'
      apply ih (derivative p).natDegree (by rw [← hn]; exact natDegree_derivative_lt hp)
        (α + 1) (β + 1) (γ - (α + β + 2)) (derivative p)
      · intro k
        convert hα (k + 1) using 1
        push_cast
        ring
      · simp only [map_add, map_sub, map_ofNat, map_one]
        simp only [map_add, map_sub, map_ofNat] at he'
        linear_combination he'
      · exact hdv
      · rfl
    have hc := eq_C_of_derivative_eq_zero hd
    have heval := congrArg (fun q : R[X] ↦ q.eval 1) hc
    simp only [eval_C, hv] at heval
    rw [hc, ← heval, C_0]

Theorem 3.2.16 Pochhammer binomial series

✓ 🤖

#

For \(a,z\in \mathbb {C}\) with \(|z|{\lt}1\),

\[ (1-z)^{-a}=\sum _{n=0}^\infty \frac{(a)_n}{n!}z^n, \]

with absolute convergence and the principal complex power. Reference: the binomial expansion used in [DLMF, 15.6.1].

Lean Formalisation

theorem Complex.choose_add_nat_sub_one_eq (a : ℂ) (n : ℕ) :
  Ring.choose (a + ↑n - 1) n = (↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n)

Lean proof

/-- Pochhammer normalization of the generalized binomial coefficient. -/
theorem choose_add_nat_sub_one_eq (a : ℂ) (n : ℕ) :
    Ring.choose (a+n-1) n = (n.factorial : ℂ)⁻¹ * (ascPochhammer ℂ n).eval a := by
  rw [← Ring.multichoose_eq]
  have h := Ring.factorial_nsmul_multichoose_eq_ascPochhammer a n
  simp only [nsmul_eq_mul] at h
  have hn : (n.factorial : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)
  apply (mul_left_cancel₀ hn)
  rw [h, ← mul_assoc, mul_inv_cancel₀ hn, one_mul]
  exact Polynomial.ascPochhammer_smeval_eq_eval a n

2 related Lean declarations

theorem Complex.hasSum_pochhammer_mul_pow (a : ℂ) {z : ℂ} (hz : ‖z‖ < 1) :
  HasSum (fun n => (↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) * z ^ n) (1 / (1 - z) ^ a)

Lean proof

/-- The binomial expansion on the unit disk, with the coefficients needed by
Euler's integral (DLMF 15.6.1). -/
theorem hasSum_pochhammer_mul_pow (a : ℂ) {z : ℂ} (hz : ‖z‖ < 1) :
    HasSum (fun n : ℕ ↦ ((n.factorial : ℂ)⁻¹ * (ascPochhammer ℂ n).eval a) * z^n)
      (1 / (1-z)^a) := by
  have h := (one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero a).hasSum
    (y := z) (by
      rw [Metric.mem_eball, edist_eq_enorm_sub, sub_zero, enorm_eq_nnnorm]
      exact_mod_cast hz)
  simpa only [FormalMultilinearSeries.ofScalars_apply_eq, smul_eq_mul,
    choose_add_nat_sub_one_eq, zero_add] using h

theorem Complex.summable_norm_pochhammer_mul_pow (a : ℂ) {z : ℂ} (hz : ‖z‖ < 1) :
  Summable fun n => ‖(↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) * z ^ n‖

Lean proof

/-- Absolute convergence of the Pochhammer binomial expansion inside its disk. -/
theorem summable_norm_pochhammer_mul_pow (a : ℂ) {z : ℂ} (hz : ‖z‖ < 1) :
    Summable (fun n : ℕ ↦ ‖((n.factorial : ℂ)⁻¹ *
      (ascPochhammer ℂ n).eval a) * z^n‖) := by
  have h := one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero a
  have hr : (‖z‖₊ : ℝ≥0∞) < 1 := by exact_mod_cast hz
  have hs := h.r_le
  have hsum := (FormalMultilinearSeries.ofScalars ℂ
    (fun n ↦ Ring.choose (a+n-1) n)).summable_norm_apply (x := z)
      (by simpa [Metric.mem_eball, edist_eq_enorm_sub, enorm_eq_nnnorm] using hr.trans_le hs)
  simpa only [FormalMultilinearSeries.ofScalars_apply_eq, smul_eq_mul,
    choose_add_nat_sub_one_eq] using hsum

Definition 3.2.17 Euler Beta integral

✓ 🤖

#

For \(a,b\in \mathbb {C}\) with \(\Re a,\Re b{\gt}0\), define

\[ B(a,b)=\int _{(0,1)} t^{a-1}(1-t)^{b-1}\, dt. \]

The powers are principal complex powers of positive real bases; the integration variable belongs to the open interval. Reference: [DLMF, 5.12.1].

Lean Formalisation

def Complex.BetaParameter : Type

Lean definition

/-- The Euler half-plane for a Beta parameter. -/
abbrev BetaParameter := {z : ℂ // 0 < z.re}

1 related Lean declaration

def Complex.betaIntegralOn (a b : Complex.BetaParameter) : ℂ

Lean definition

/-- The classical Euler Beta integral, without endpoint power assignments. -/
def betaIntegralOn (a b : BetaParameter) : ℂ :=
  ∫ t : Ioo (0 : ℝ) 1, (t.val : ℂ) ^ (a.val - 1) *
    (1 - (t.val : ℂ)) ^ (b.val - 1) ∂Measure.comap Subtype.val volume

Theorem 3.2.18 Characterisation of the Euler Beta integral

✓ 🤖

#

For every pair in the preceding domain the integrand is integrable, and

\[ B(a,b)=\frac{\Gamma (a)\Gamma (b)}{\Gamma (a+b)}\ne 0. \]

All three Gamma arguments lie in the open right half-plane. Reference: [DLMF, 5.12.1].

Lean Formalisation

theorem Complex.integrable_betaIntegralOn (a b : Complex.BetaParameter) :
  MeasureTheory.Integrable (fun t => ↑↑t ^ (↑a - 1) * (1 - ↑↑t) ^ (↑b - 1))
    (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)

Lean proof

/-- Every input in the typed domain gives an integrable Beta integrand. -/
theorem integrable_betaIntegralOn (a b : BetaParameter) :
    Integrable (fun t : Ioo (0 : ℝ) 1 ↦ (t.val : ℂ) ^ (a.val - 1) *
      (1 - (t.val : ℂ)) ^ (b.val - 1)) (Measure.comap Subtype.val volume) := by
  obtain ⟨B,hB,hi⟩ := exists_beta_representative a b
  have hI := (intervalIntegrable_iff_integrableOn_Ioo_of_le (f := B) (by norm_num : (0 : ℝ) ≤ 1)).mp hi
  have h := (integrableOn_iff_comap_subtypeVal (f := B) (μ := volume) measurableSet_Ioo).mp hI
  apply h.congr
  filter_upwards [] with t
  exact hB t

2 related Lean declarations

theorem Complex.betaIntegralOn_eq_Gamma (a b : Complex.BetaParameter) :
  Complex.betaIntegralOn a b =
    Complex.GammaOn (Complex.GammaPoint.ofRePos ↑a ⋯) * Complex.GammaOn (Complex.GammaPoint.ofRePos ↑b ⋯) /
      Complex.GammaOn (Complex.GammaPoint.ofRePos (↑a + ↑b) ⋯)

Lean proof

/-- The Beta--Gamma formula uses only Gamma values in the right half-plane. -/
theorem betaIntegralOn_eq_Gamma (a b : BetaParameter) :
    betaIntegralOn a b = GammaOn (.ofRePos a.val a.property) *
      GammaOn (.ofRePos b.val b.property) /
        GammaOn (.ofRePos (a.val + b.val) (by
          rw [add_re]; exact add_pos a.property b.property)) := by
  apply (eq_div_iff (GammaOn_ne_zero _)).mpr
  simpa only [GammaOn, GammaPoint.ofRePos, mul_comm] using (safe_gamma_beta a b).symm

theorem Complex.betaIntegralOn_ne_zero (a b : Complex.BetaParameter) : Complex.betaIntegralOn a b ≠ 0

Lean proof

/-- The Euler Beta value is nonzero throughout its classical domain. -/
theorem betaIntegralOn_ne_zero (a b : BetaParameter) : betaIntegralOn a b ≠ 0 := by
  rw [betaIntegralOn_eq_Gamma]
  exact div_ne_zero (mul_ne_zero (GammaOn_ne_zero _) (GammaOn_ne_zero _)) (GammaOn_ne_zero _)

Theorem 3.2.19 Euler Beta moments

✓ 🤖

#

For \(\Re b{\gt}0\), \(\Re (c-b){\gt}0\), and \(n\in \mathbb {N}\),

\[ B(b+n,c-b)=B(b,c-b)\frac{(b)_n}{(c)_n}. \]

Thus integration of \(t^n\) against \(t^{b-1}(1-t)^{c-b-1}\), followed by multiplication by \((a)_n/n!\), gives \(B(b,c-b)\) times the \(n\)th ordinary Gauss-series coefficient. These integrands are integrable on \((0,1)\). More generally, the shifted moment \(\int _{(0,1)}t^{u-n-1}(1-t)^{v-1}t^n\, dt=B(u,v)\) is integrable for \(\Re u,\Re v{\gt}0\), even when the unshifted exponent would not be integrable. The Euler parameters \((a,b,b+d)\) are admissible whenever \(\Re b,\Re d{\gt}0\). Reference: [DLMF, 5.12.1, 15.6.1].

Lean Formalisation

theorem Complex.betaIntegralOn_add_nat_left (a b : Complex.BetaParameter) (n : ℕ) :
  Complex.betaIntegralOn ⟨↑a + ↑n, ⋯⟩ b =
    Complex.betaIntegralOn a b * Polynomial.eval (↑a) (ascPochhammer ℂ n) /
      Polynomial.eval (↑a + ↑b) (ascPochhammer ℂ n)

Lean proof

/-- The classical Beta shift formula on its full Euler domain. -/
theorem betaIntegralOn_add_nat_left (a b : BetaParameter) (n : ℕ) :
    betaIntegralOn ⟨a.val + n, by simp only [add_re, natCast_re]; exact add_pos_of_pos_of_nonneg a.property (Nat.cast_nonneg _)⟩ b =
      betaIntegralOn a b * (ascPochhammer ℂ n).eval a.val /
        (ascPochhammer ℂ n).eval (a.val + b.val) := by
  have hc : 0 < (a.val+b.val).re := by simpa only [add_re] using add_pos a.property b.property
  have hga := GammaOn_ne_zero (GammaPoint.ofRePos a.val a.property)
  have hgc := GammaOn_ne_zero (GammaPoint.ofRePos (a.val+b.val) hc)
  have hgcn := GammaOn_ne_zero ((GammaPoint.ofRePos (a.val+b.val) hc).addNat n)
  have hra := GammaOn_add_nat_div (GammaPoint.ofRePos a.val a.property) n
  have hrc := GammaOn_add_nat_div (GammaPoint.ofRePos (a.val+b.val) hc) n
  rw [betaIntegralOn_eq_Gamma,betaIntegralOn_eq_Gamma]
  simp only [GammaOn,GammaPoint.ofRePos,GammaPoint.addNat_val] at hga hgc hgcn hra hrc ⊢
  rw [← hra,← hrc,show a.val+n+b.val = a.val+b.val+n by ring]
  field_simp

3 related Lean declarations

theorem Complex.integral_betaWeight_mul_powOn (a b : Complex.BetaParameter) (n : ℕ) :
  MeasureTheory.Integrable (fun t => ↑↑t ^ (↑a - ↑n - 1) * (1 - ↑↑t) ^ (↑b - 1) * ↑↑t ^ n)
      (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧
    ∫ (t : ↑(Set.Ioo 0 1)),
        ↑↑t ^ (↑a - ↑n - 1) * (1 - ↑↑t) ^ (↑b - 1) *
          ↑↑t ^ n ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume =
      Complex.betaIntegralOn a b

Lean proof

/-- Shifted Beta moments retain cases whose unshifted first parameter is not integrable. -/
theorem integral_betaWeight_mul_powOn (a b : BetaParameter) (n : ℕ) :
    Integrable (fun t : Ioo (0 : ℝ) 1 ↦
      ((t.val : ℂ) ^ (a.val - n - 1) * (1 - (t.val : ℂ)) ^ (b.val - 1)) *
        (t.val : ℂ) ^ n) (Measure.comap Subtype.val volume) ∧
    (∫ t : Ioo (0 : ℝ) 1,
      ((t.val : ℂ) ^ (a.val - n - 1) * (1 - (t.val : ℂ)) ^ (b.val - 1)) *
        (t.val : ℂ) ^ n ∂Measure.comap Subtype.val volume) = betaIntegralOn a b := by
  have he : (fun t : Ioo (0 : ℝ) 1 ↦
      ((t.val : ℂ) ^ (a.val - n - 1) * (1 - (t.val : ℂ)) ^ (b.val - 1)) *
        (t.val : ℂ) ^ n) =
      (fun t : Ioo (0 : ℝ) 1 ↦ (t.val : ℂ) ^ (a.val - 1) *
        (1 - (t.val : ℂ)) ^ (b.val - 1)) := by
    funext t
    have ht : (t.val : ℂ) ≠ 0 := ofReal_ne_zero.mpr t.property.1.ne'
    rw [mul_right_comm, ← cpow_natCast, ← cpow_add _ _ ht]
    congr 2
    ring
  rw [he]
  exact ⟨integrable_betaIntegralOn a b, rfl⟩

def Complex.eulerGaussParameters (a : ℂ) (b d : Complex.BetaParameter) : GaussParameters ℂ

Lean definition

/-- Positive Euler parameters certify the Gauss denominator. -/
def eulerGaussParameters (a : ℂ) (b d : BetaParameter) : GaussParameters ℂ :=
  .ofNoPole a b.val (b.val + d.val)
    (GammaPoint.ofRePos _ (by simpa only [add_re] using add_pos b.property d.property)).property

theorem Complex.integral_eulerHypergeometric_termOn (a : ℂ) (b d : Complex.BetaParameter) (n : ℕ) :
  MeasureTheory.Integrable
      (fun t =>
        (↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) * (↑↑t ^ (↑b - 1) * (1 - ↑↑t) ^ (↑d - 1) * ↑↑t ^ n))
      (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧
    ∫ (t : ↑(Set.Ioo 0 1)),
        (↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) *
          (↑↑t ^ (↑b - 1) * (1 - ↑↑t) ^ (↑d - 1) *
            ↑↑t ^ n) ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume =
      Complex.betaIntegralOn b d * ordinaryHypergeometricCoefficientOn (a.eulerGaussParameters b d) n

Lean proof

/-- The Euler coefficient moment uses the admissible Gauss coefficient. -/
theorem integral_eulerHypergeometric_termOn (a : ℂ) (b d : BetaParameter) (n : ℕ) :
    Integrable (fun t : Ioo (0 : ℝ) 1 ↦
      ((n.factorial : ℂ)⁻¹*(ascPochhammer ℂ n).eval a) *
        (((t.val : ℂ)^(b.val-1)*(1-(t.val : ℂ))^(d.val-1))*(t.val : ℂ)^n))
      (Measure.comap Subtype.val volume) ∧
    (∫ t : Ioo (0 : ℝ) 1,
      ((n.factorial : ℂ)⁻¹*(ascPochhammer ℂ n).eval a) *
        (((t.val : ℂ)^(b.val-1)*(1-(t.val : ℂ))^(d.val-1))*(t.val : ℂ)^n)
      ∂Measure.comap Subtype.val volume) =
      betaIntegralOn b d * ordinaryHypergeometricCoefficientOn (eulerGaussParameters a b d) n := by
  let bn : BetaParameter := ⟨b.val+n, by
    simp only [add_re,natCast_re]
    exact add_pos_of_pos_of_nonneg b.property (Nat.cast_nonneg _)⟩
  have h := integral_betaWeight_mul_powOn bn d n
  have he : bn.val-n-1 = b.val-1 := by dsimp only [bn]; ring
  simp only [he] at h
  refine ⟨h.1.const_mul _, ?_⟩
  rw [integral_const_mul, h.2]
  have hcn : (ascPochhammer ℂ n).eval (eulerGaussParameters a b d).c ≠ 0 := by
    intro hz
    obtain ⟨k,_,hk⟩ := (ascPochhammer_eval_eq_zero_iff _ _).mp hz
    have hr := congrArg Complex.re hk
    simp only [eulerGaussParameters, GaussParameters.ofNoPole, natCast_re, neg_re, add_re] at hr
    linarith [b.property, d.property, Nat.cast_nonneg (α := ℝ) k]
  rw [betaIntegralOn_add_nat_left, ordinaryHypergeometricCoefficientOn_eq_div _ n hcn]
  dsimp only [eulerGaussParameters,GaussParameters.ofNoPole]
  ring

Theorem 3.2.20 Euler integral for the Gauss function

✓ 🤖

#

Let \(a,b,c,z\in \mathbb {C}\), \(\Re b{\gt}0\), \(\Re (c-b){\gt}0\), and \(|z|{\lt}1\). Then

\[ \int _0^1\frac{t^{b-1}(1-t)^{c-b-1}}{(1-zt)^a}\, dt = B(b,c-b)\, {}_2F_1(a,b;c;z) = \Gamma (b)\Gamma (c-b)\, \mathbf F(a,b;c;z). \]

All integrals here are over \((0,1)\) and their integrability is asserted. The real and complex definitions agree on real parameters and arguments, and the same integral formula holds over the reals. The dominated-convergence lemma takes any complex \(L^1(0,1)\) weight and asserts integrability of each term and of the summed integrand, together with the sum identity. Reference: [DLMF, 15.6.1], which prints the regularized normalization.

Lean Formalisation

theorem Complex.hasSum_integral_binomialOn (a : ℂ) (z : ↑(Metric.ball 0 1))
  (w : ↥(MeasureTheory.Lp ℂ 1 (MeasureTheory.volume.restrict (Set.Ioo 0 1)))) :
  (∀ (n : ℕ),
      MeasureTheory.Integrable
        (fun t => ↑↑w ↑t * ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) * (↑z * ↑↑t) ^ n))
        (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)) ∧
    MeasureTheory.Integrable (fun t => ↑↑w ↑t / (1 - ↑z * ↑↑t) ^ a)
        (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧
      HasSum
        (fun n =>
          ∫ (t : ↑(Set.Ioo 0 1)),
            ↑↑w ↑t *
              ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer ℂ n) *
                (↑z * ↑↑t) ^ n) ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)
        (∫ (t : ↑(Set.Ioo 0 1)),
          ↑↑w ↑t / (1 - ↑z * ↑↑t) ^ a ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)

Lean proof

/-- The weighted binomial integral asserts integrability together with its sum. -/
theorem hasSum_integral_binomialOn (a : ℂ) (z : Metric.ball (0 : ℂ) 1)
    (w : Lp ℂ 1 (volume.restrict (Ioo (0 : ℝ) 1))) :
    (∀ n : ℕ, Integrable (fun t : Ioo (0 : ℝ) 1 ↦
      w t.val * (((n.factorial : ℂ)⁻¹ * (ascPochhammer ℂ n).eval a) *
        (z.val * (t.val : ℂ)) ^ n)) (Measure.comap Subtype.val volume)) ∧
    Integrable (fun t : Ioo (0 : ℝ) 1 ↦ w t.val / (1 - z.val * (t.val : ℂ)) ^ a)
      (Measure.comap Subtype.val volume) ∧
    HasSum (fun n : ℕ ↦ ∫ t : Ioo (0 : ℝ) 1,
      w t.val * (((n.factorial : ℂ)⁻¹ * (ascPochhammer ℂ n).eval a) *
        (z.val * (t.val : ℂ)) ^ n) ∂Measure.comap Subtype.val volume)
      (∫ t : Ioo (0 : ℝ) 1, w t.val / (1 - z.val * (t.val : ℂ)) ^ a
        ∂Measure.comap Subtype.val volume) := by
  have hz : ‖z.val‖ < 1 := by simpa only [Metric.mem_ball, dist_zero_right] using z.property
  have hw : IntervalIntegrable (fun t ↦ w t) volume 0 1 :=
    (intervalIntegrable_iff_integrableOn_Ioo_of_le (by norm_num : (0 : ℝ) ≤ 1)).mpr
      (memLp_one_iff_integrable.mp (Lp.memLp w))
  have hi (n : ℕ) : IntervalIntegrable (fun t : ℝ ↦
      w t * (((n.factorial : ℂ)⁻¹ * (ascPochhammer ℂ n).eval a) *
        (z.val * (t : ℂ)) ^ n)) volume 0 1 := hw.mul_continuousOn (by fun_prop)
  have hj := intervalIntegrable_div_eulerFactor a hz hw
  refine ⟨fun n ↦ ?_, ?_, ?_⟩
  · have h := (intervalIntegrable_iff_integrableOn_Ioo_of_le (by norm_num : (0 : ℝ) ≤ 1)).mp (hi n)
    exact (integrableOn_iff_comap_subtypeVal measurableSet_Ioo).mp h
  · have h := (intervalIntegrable_iff_integrableOn_Ioo_of_le (by norm_num : (0 : ℝ) ≤ 1)).mp hj
    exact (integrableOn_iff_comap_subtypeVal measurableSet_Ioo).mp h
  · convert hasSum_integral_binomial a hz hw using 1
    · funext n
      exact integral_open_unit_eq_interval _ (hi n)
    · exact integral_open_unit_eq_interval _ hj

5 related Lean declarations

theorem Complex.integral_eulerHypergeometricOn (a : ℂ) (b d : Complex.BetaParameter) (z : ↑(Metric.ball 0 1)) :
  MeasureTheory.Integrable (fun t => ↑↑t ^ (↑b - 1) * (1 - ↑↑t) ^ (↑d - 1) / (1 - ↑z * ↑↑t) ^ a)
      (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧
    ∫ (t : ↑(Set.Ioo 0 1)),
        ↑↑t ^ (↑b - 1) * (1 - ↑↑t) ^ (↑d - 1) /
          (1 - ↑z * ↑↑t) ^ a ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume =
      Complex.betaIntegralOn b d *
        ordinaryHypergeometricOn (a.eulerGaussParameters b d)
          (GaussSeriesPoint.ofUnitDisk (a.eulerGaussParameters b d) z)

Lean proof

/-- Euler's integral together with its integrability, on the classical domain. -/
theorem integral_eulerHypergeometricOn (a : ℂ) (b d : BetaParameter)
    (z : Metric.ball (0 : ℂ) 1) :
    Integrable (fun t : Ioo (0 : ℝ) 1 ↦
      ((t.val : ℂ)^(b.val-1)*(1-(t.val : ℂ))^(d.val-1)) /
        (1-z.val*(t.val : ℂ))^a) (Measure.comap Subtype.val volume) ∧
    (∫ t : Ioo (0 : ℝ) 1,
      ((t.val : ℂ)^(b.val-1)*(1-(t.val : ℂ))^(d.val-1)) /
        (1-z.val*(t.val : ℂ))^a ∂Measure.comap Subtype.val volume) =
      betaIntegralOn b d * ordinaryHypergeometricOn (eulerGaussParameters a b d)
        (.ofUnitDisk _ z) := by
  let W : ℝ → ℂ := fun t ↦ if h : t ∈ Ioo (0 : ℝ) 1 then
    (t : ℂ)^(b.val-1)*(1-(t : ℂ))^(d.val-1) else 0
  have hW (t : Ioo (0 : ℝ) 1) : W t.val =
      (t.val : ℂ)^(b.val-1)*(1-(t.val : ℂ))^(d.val-1) := by
    simp only [W,dite_eq_left t.property]
  have hiW : IntegrableOn W (Ioo (0 : ℝ) 1) volume := by
    apply (integrableOn_iff_comap_subtypeVal (f := W) (μ := volume) measurableSet_Ioo).mpr
    apply (integrable_betaIntegralOn b d).congr
    filter_upwards [] with t
    exact (hW t).symm
  let w := (memLp_one_iff_integrable.mpr hiW).toLp W
  have hew : (fun t : Ioo (0 : ℝ) 1 ↦ w t.val) =ᵐ[Measure.comap Subtype.val volume]
      (fun t ↦ (t.val : ℂ)^(b.val-1)*(1-(t.val : ℂ))^(d.val-1)) := by
    have hw := (ae_restrict_iff_subtype measurableSet_Ioo).mp
      (memLp_one_iff_integrable.mpr hiW).coeFn_toLp
    filter_upwards [hw] with t ht
    exact ht.trans (hW t)
  obtain ⟨hterms,hint,hsum⟩ := hasSum_integral_binomialOn a z w
  have heval : (∫ t : Ioo (0 : ℝ) 1, w t.val / (1-z.val*(t.val : ℂ))^a
      ∂Measure.comap Subtype.val volume) =
      (∫ t : Ioo (0 : ℝ) 1,
      ((t.val : ℂ)^(b.val-1)*(1-(t.val : ℂ))^(d.val-1)) /
        (1-z.val*(t.val : ℂ))^a ∂Measure.comap Subtype.val volume) := by
    apply integral_congr_ae
    filter_upwards [hew] with t ht
    rw [ht]
  refine ⟨hint.congr ?_, ?_⟩
  · filter_upwards [hew] with t ht
    rw [ht]
  · have hterm (n : ℕ) : (∫ t : Ioo (0 : ℝ) 1,
        w t.val * (((n.factorial : ℂ)⁻¹ * (ascPochhammer ℂ n).eval a) *
          (z.val * (t.val : ℂ)) ^ n) ∂Measure.comap Subtype.val volume) =
        betaIntegralOn b d * (ordinaryHypergeometricCoefficientOn (eulerGaussParameters a b d) n * z.val^n) := by
      calc
        _ = (∫ t : Ioo (0 : ℝ) 1,
            (((n.factorial : ℂ)⁻¹*(ascPochhammer ℂ n).eval a) *
            (((t.val : ℂ)^(b.val-1)*(1-(t.val : ℂ))^(d.val-1))*(t.val : ℂ)^n)) * z.val^n
            ∂Measure.comap Subtype.val volume) := by
          apply integral_congr_ae
          filter_upwards [hew] with t ht
          rw [ht,mul_pow]
          ring
        _ = _ := by rw [integral_mul_const,(integral_eulerHypergeometric_termOn a b d n).2,mul_assoc]
    simp_rw [hterm] at hsum
    rw [heval] at hsum
    exact hsum.unique ((hasSum_ordinaryHypergeometricOn (eulerGaussParameters a b d) z).mul_left _)

theorem Complex.integral_eulerRegularizedHypergeometricOn (a : ℂ) (b d : Complex.BetaParameter) (z : ↑(Metric.ball 0 1)) :
  let c := Complex.GammaPoint.ofRePos (↑b + ↑d) ⋯;
  ∫ (t : ↑(Set.Ioo 0 1)),
      ↑↑t ^ (↑b - 1) * (1 - ↑↑t) ^ (↑d - 1) /
        (1 - ↑z * ↑↑t) ^ a ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume =
    Complex.GammaOn (Complex.GammaPoint.ofRePos ↑b ⋯) * Complex.GammaOn (Complex.GammaPoint.ofRePos ↑d ⋯) *
      a.regularizedGaussHGFunOn (↑b) (↑c)
        (Complex.RegularizedHGSeriesPoint.ofGauss a (↑b) c (GaussSeriesPoint.ofUnitDisk (a.eulerGaussParameters b d) z))

Lean proof

/-- Euler's classical integral in regularized normalization. -/
theorem integral_eulerRegularizedHypergeometricOn (a : ℂ) (b d : BetaParameter)
    (z : Metric.ball (0 : ℂ) 1) :
    let c := GammaPoint.ofRePos (b.val+d.val)
      (by simpa only [add_re] using add_pos b.property d.property)
    (∫ t : Ioo (0 : ℝ) 1,
      ((t.val : ℂ)^(b.val-1)*(1-(t.val : ℂ))^(d.val-1)) /
        (1-z.val*(t.val : ℂ))^a ∂Measure.comap Subtype.val volume) =
      GammaOn (.ofRePos b.val b.property) * GammaOn (.ofRePos d.val d.property) *
        regularizedGaussHGFunOn a b.val c.val
          (.ofGauss a b.val c (.ofUnitDisk (eulerGaussParameters a b d) z)) := by
  dsimp only
  rw [(integral_eulerHypergeometricOn a b d z).2, betaIntegralOn_eq_Gamma]
  dsimp only [eulerGaussParameters]
  erw [← ordinaryHypergeometricOn_div_Gamma_eq]
  dsimp only [GammaPoint.ofRePos]
  ring

theorem Complex.ofReal_ascPochhammer_eval (a : ℝ) (n : ℕ) :
  ↑(Polynomial.eval a (ascPochhammer ℝ n)) = Polynomial.eval (↑a) (ascPochhammer ℂ n)

Lean proof

/-- Real ascending Pochhammer evaluations embed into the complex ones. -/
theorem ofReal_ascPochhammer_eval (a : ℝ) (n : ℕ) :
    (((ascPochhammer ℝ n).eval a : ℝ) : ℂ) = (ascPochhammer ℂ n).eval (a : ℂ) := by
  induction n with
  | zero => simp
  | succ n ih => simp [ascPochhammer_succ_eval, ih]

def Real.eulerGaussParameters (a : ℝ) (b d : ↑(Set.Ioi 0)) : GaussParameters ℝ

Lean definition

/-- The real Euler parameters give an admissible classical Gauss series. -/
def eulerGaussParameters (a : ℝ) (b d : Ioi (0 : ℝ)) : GaussParameters ℝ :=
  .ofNoPole a b.val (b.val+d.val) (GammaPoint.ofPos _ (add_pos b.property d.property)).property

theorem Real.integral_eulerHypergeometricOn (a : ℝ) (b d : ↑(Set.Ioi 0)) (z : ↑(Metric.ball 0 1)) :
  MeasureTheory.Integrable (fun t => ↑t ^ (↑b - 1) * (1 - ↑t) ^ (↑d - 1) / (1 - ↑z * ↑t) ^ a)
      (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧
    ∫ (t : ↑(Set.Ioo 0 1)),
        ↑t ^ (↑b - 1) * (1 - ↑t) ^ (↑d - 1) /
          (1 - ↑z * ↑t) ^ a ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume =
      Real.GammaOn (Real.GammaPoint.ofPos ↑b ⋯) * Real.GammaOn (Real.GammaPoint.ofPos ↑d ⋯) /
          Real.GammaOn (Real.GammaPoint.ofPos (↑b + ↑d) ⋯) *
        ordinaryHypergeometricOn (a.eulerGaussParameters b d)
          (GaussSeriesPoint.ofUnitDisk (a.eulerGaussParameters b d) z)

Lean proof

/-- The real Euler integral has its actual integrability and classical value. -/
theorem integral_eulerHypergeometricOn (a : ℝ) (b d : Ioi (0 : ℝ))
    (z : Metric.ball (0 : ℝ) 1) :
    Integrable (fun t : Ioo (0 : ℝ) 1 ↦
      t.val^(b.val-1)*(1-t.val)^(d.val-1)/(1-z.val*t.val)^a)
      (Measure.comap Subtype.val volume) ∧
    (∫ t : Ioo (0 : ℝ) 1,
      t.val^(b.val-1)*(1-t.val)^(d.val-1)/(1-z.val*t.val)^a
      ∂Measure.comap Subtype.val volume) =
      (GammaOn (.ofPos b.val b.property) * GammaOn (.ofPos d.val d.property) /
        GammaOn (.ofPos (b.val+d.val) (add_pos b.property d.property))) *
        ordinaryHypergeometricOn (eulerGaussParameters a b d) (.ofUnitDisk _ z) := by
  have hz : |z.val| < 1 := by simpa only [Metric.mem_ball, dist_zero_right, Real.norm_eq_abs] using z.property
  let bc : Complex.BetaParameter := ⟨(b.val : ℂ), b.property⟩
  let dc : Complex.BetaParameter := ⟨(d.val : ℂ), d.property⟩
  let zc : Metric.ball (0 : ℂ) 1 := ⟨(z.val : ℂ), by simpa using hz⟩
  have he (t : Ioo (0 : ℝ) 1) :
      ((t.val : ℂ)^(bc.val-1)*(1-(t.val : ℂ))^(dc.val-1)) /
        (1-zc.val*(t.val : ℂ))^(a : ℂ) =
      ((t.val^(b.val-1)*(1-t.val)^(d.val-1)/(1-z.val*t.val)^a : ℝ) : ℂ) := by
    have hp : 0 < 1-z.val*t.val := by
      have h₁ := mul_le_mul_of_nonneg_right (le_abs_self z.val) t.property.1.le
      have h₂ := (mul_le_of_le_one_right (abs_nonneg z.val) t.property.2.le).trans_lt hz
      linarith
    dsimp [bc, dc, zc]
    rw [Complex.ofReal_div, Complex.ofReal_mul,
      Complex.ofReal_cpow t.property.1.le,
      Complex.ofReal_cpow (by linarith [t.property.2] : 0 ≤ 1-t.val),
      Complex.ofReal_cpow hp.le]
    push_cast
    rfl
  have hc := (Complex.integral_eulerHypergeometricOn (a : ℂ) bc dc zc).1
  have hi : Integrable (fun t : Ioo (0 : ℝ) 1 ↦
      t.val^(b.val-1)*(1-t.val)^(d.val-1)/(1-z.val*t.val)^a)
      (Measure.comap Subtype.val volume) := by
    have h := Complex.reCLM.integrable_comp hc
    simpa only [he, Complex.reCLM_apply, Complex.ofReal_re] using h
  refine ⟨hi, ?_⟩
  have hp : (eulerGaussParameters a b d).toComplex =
      Complex.eulerGaussParameters (a : ℂ) bc dc := by
    simp only [eulerGaussParameters,GaussParameters.toComplex,
      Complex.eulerGaussParameters,GaussParameters.ofNoPole,bc,dc,Complex.ofReal_add]
  have hv : ((ordinaryHypergeometricOn (eulerGaussParameters a b d) (.ofUnitDisk _ z) : ℝ) : ℂ) =
      ordinaryHypergeometricOn (Complex.eulerGaussParameters (a : ℂ) bc dc) (.ofUnitDisk _ zc) := by
    rw [Complex.ofReal_ordinaryHypergeometric]
    have hpoint : ((GaussSeriesPoint.ofUnitDisk (eulerGaussParameters a b d) z).toComplex
        (eulerGaussParameters a b d)).val = zc.val := rfl
    generalize hzz : (GaussSeriesPoint.ofUnitDisk (eulerGaussParameters a b d) z).toComplex
      (eulerGaussParameters a b d) = zz at *
    clear hzz
    revert zz
    rw [hp]
    intro zz hpoint
    congr 1
    exact Subtype.ext hpoint
  apply Complex.ofReal_injective
  rw [Complex.ofReal_mul,hv]
  have hvalue := (Complex.integral_eulerHypergeometricOn (a : ℂ) bc dc zc).2
  rw [Complex.betaIntegralOn_eq_Gamma] at hvalue
  calc
    _ = (∫ t : Ioo (0 : ℝ) 1,
      ((t.val : ℂ)^(bc.val-1)*(1-(t.val : ℂ))^(dc.val-1)) /
        (1-zc.val*(t.val : ℂ))^(a : ℂ) ∂Measure.comap Subtype.val volume) := by
      rw [← integral_complex_ofReal]
      apply integral_congr_ae
      filter_upwards [] with t
      exact (he t).symm
    _ = _ := by
      rw [hvalue]
      simp only [Complex.GammaOn,Complex.GammaPoint.ofRePos,GammaOn,GammaPoint.ofPos,
        bc,dc,← Complex.ofReal_add,Complex.Gamma_ofReal,Complex.ofReal_div,Complex.ofReal_mul]

Theorem 3.2.21 Symmetric Jacobi coefficient parity

✓ 🤖

#

The coefficient of \(x^j\) in \(P_n^{(\beta ,\beta )}\) vanishes if \(j\) and \(n\) have different parity, for every real \(\beta \), including degenerate parameters.

Reference: [DLMF, Table 18.6.1].

Lean Formalisation

theorem Polynomial.coeff_comp_neg_X.{u_1} {R : Type u_1} [CommRing R] (p : Polynomial R) (j : ℕ) :
  (p.comp (-Polynomial.X)).coeff j = (-1) ^ j * p.coeff j

Lean proof

/-- Reflection multiplies each coefficient by the parity of its index. -/
theorem coeff_comp_neg_X {R : Type*} [CommRing R] (p : R[X]) (j : ℕ) :
    (p.comp (-X)).coeff j = (-1 : R) ^ j * p.coeff j := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq, mul_add]
  | monomial k a =>
    have hpow : (-X : R[X]) ^ k = C ((-1 : R) ^ k) * X ^ k := by
      rw [show (-X : R[X]) = C (-1 : R) * X by simp, mul_pow, ← map_pow]
    rw [monomial_comp, hpow]
    simp only [coeff_C_mul, coeff_X_pow, coeff_monomial]
    by_cases h : j = k
    · subst j
      simp [mul_comm]
    · simp [h, Ne.symm h]

1 related Lean declaration

theorem Polynomial.coeff_jacobi_symmetric_eq_zero_of_parity (β : ℝ) (n j : ℕ) (h : j % 2 ≠ n % 2) :
  (Polynomial.jacobi β β n).coeff j = 0

Lean proof

/-- Symmetric real Jacobi coefficients of the wrong parity vanish, including
parameter values where the polynomial degenerates. -/
theorem coeff_jacobi_symmetric_eq_zero_of_parity (β : ℝ) (n j : ℕ)
    (h : j % 2 ≠ n % 2) : (jacobi β β n).coeff j = 0 := by
  have he := congrArg (fun p : ℝ[X] => p.coeff j) (jacobi_comp_neg_X β β n)
  rw [coeff_comp_neg_X, coeff_C_mul] at he
  rw [neg_one_pow_eq_pow_mod_two j, neg_one_pow_eq_pow_mod_two n] at he
  have hj : j % 2 < 2 := Nat.mod_lt _ (by norm_num)
  have hn : n % 2 < 2 := Nat.mod_lt _ (by norm_num)
  have hc : (j % 2 = 0 ∧ n % 2 = 1) ∨ (j % 2 = 1 ∧ n % 2 = 0) := by omega
  rcases hc with ⟨hj, hn⟩ | ⟨hj, hn⟩ <;>
    rw [hj, hn] at he <;> simp only [pow_zero, pow_one, one_mul, neg_one_mul] at he <;>
    linarith

3.2.3 Orthogonality and zeros

For \(\alpha ,\beta {\gt}-1\), the Jacobi weight is integrable and the polynomials are orthogonal. The degree-zero norm has a separate formula, valid also when \(\alpha +\beta +1=0\).

Theorem 3.2.22 Jacobi weight integrability

✓ 🙂 human-reviewed

#

For \(\alpha ,\beta {\gt}-1\), the weight is integrable on \((-1,1)\) and every real-valued function continuous on \([-1,1]\) is \(\mu _{\alpha ,\beta }\)-integrable.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integrable_jacobiWeight {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  MeasureTheory.Integrable (fun x => ↑((Polynomial.jacobiWeight α β) x)) MeasureTheory.volume

Lean proof

/-- All classically integrable endpoint singularities are included (DLMF 18.3.1). -/
theorem integrable_jacobiWeight {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
    Integrable (fun x : Ioo (-1 : ℝ) 1 ↦ (jacobiWeight α β x : ℝ)) volume := by
  let P : ℝ → ℝ → ℝ := fun a t ↦ if 0 < t then t ^ a else 0
  have hp (a : ℝ) (ha : -1 < a) : IntervalIntegrable (P a) volume 0 1 := by
    rw [intervalIntegrable_iff_integrableOn_Ioo_of_le (by norm_num : (0 : ℝ) ≤ 1)]
    have hraw : IntegrableOn (fun x : ℝ ↦ x ^ a) (Ioo (0 : ℝ) 1) := by
      have h := (integrableOn_iff_comap_subtypeVal (f := fun x : ℝ ↦ x ^ a)
        measurableSet_Ioo).mpr (Real.integrable_rpow_openInterval ⟨a, ha⟩ 0 1)
      simpa using h
    apply hraw.congr_fun
    · intro x hx
      simp [P, hx.1]
    · exact measurableSet_Ioo
  have hl : IntervalIntegrable (fun x : ℝ ↦ P β (1 + x)) volume (-1) 0 := by
    simpa using (hp β hβ).comp_add_left 1
  have hr : IntervalIntegrable (fun x : ℝ ↦ P α (1 - x)) volume 0 1 := by
    simpa using ((hp α hα).comp_sub_left 1).symm
  have hi : IntervalIntegrable (fun x : ℝ ↦ P α (1 - x) * P β (1 + x)) volume (-1) 1 := by
    apply IntervalIntegrable.trans (b := 0)
    · have hreg : ContinuousOn (fun x : ℝ ↦ (1 - x) ^ α) (uIcc (-1) 0) := by
        apply continuousOn_of_forall_continuousAt
        intro x hx
        rw [uIcc_of_le (by norm_num : (-1 : ℝ) ≤ 0)] at hx
        exact (continuousAt_const.sub continuousAt_id).rpow_const
          (Or.inl (by change 1 - x ≠ 0; linarith [hx.2]))
      apply (hl.continuousOn_mul hreg).congr
      intro x hx
      rw [uIoc_of_le (by norm_num : (-1 : ℝ) ≤ 0)] at hx
      simp [P, show 0 < 1 - x by linarith [hx.2]]
    · have hreg : ContinuousOn (fun x : ℝ ↦ (1 + x) ^ β) (uIcc 0 1) := by
        apply continuousOn_of_forall_continuousAt
        intro x hx
        rw [uIcc_of_le (by norm_num : (0 : ℝ) ≤ 1)] at hx
        exact (continuousAt_const.add continuousAt_id).rpow_const
          (Or.inl (by change 1 + x ≠ 0; linarith [hx.1]))
      apply (hr.mul_continuousOn hreg).congr
      intro x hx
      rw [uIoc_of_le (by norm_num : (0 : ℝ) ≤ 1)] at hx
      simp [P, show 0 < 1 + x by linarith [hx.1]]
  rw [intervalIntegrable_iff_integrableOn_Ioo_of_le (by norm_num : (-1 : ℝ) ≤ 1),
    integrableOn_iff_comap_subtypeVal measurableSet_Ioo] at hi
  apply hi.congr
  filter_upwards [] with x
  dsimp [Function.comp_def, P]
  rw [ite_eq_left (show 0 < 1 - (x : ℝ) by linarith [x.property.2]),
    ite_eq_left (show 0 < 1 + (x : ℝ) by linarith [x.property.1])]
  rfl

1 related Lean declaration

theorem Polynomial.integrable_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) {f : ℝ → ℝ}
  (hf : ContinuousOn f (Set.Icc (-1) 1)) : MeasureTheory.Integrable f (Polynomial.jacobiMeasure α β)

Lean proof

/-- Continuous functions on the closed interval are Jacobi-integrable
(DLMF Table 18.3.1). -/
theorem integrable_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β)
    {f : ℝ → ℝ} (hf : ContinuousOn f (Icc (-1) 1)) : Integrable f (jacobiMeasure α β) := by
  rw [integrable_jacobiMeasure_iff]
  obtain ⟨C, hC⟩ := isCompact_Icc.exists_bound_of_continuousOn hf
  have hc : Continuous (fun x : Ioo (-1 : ℝ) 1 ↦ f x) :=
    continuousOn_iff_continuous_domRestrict.mp (hf.mono Ioo_subset_Icc_self)
  exact (integrable_jacobiWeight hα hβ).mul_bdd hc.aestronglyMeasurable
    (Filter.Eventually.of_forall fun x ↦ hC x (Ioo_subset_Icc_self x.property))

Theorem 3.2.23 Jacobi pairwise orthogonality

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\) and distinct \(m,n\), \(\int P_m^{(\alpha ,\beta )}P_n^{(\alpha ,\beta )}\, d\mu _{\alpha ,\beta }=0\). The sequence satisfies the general orthogonality predicate.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integral_mul_jacobi_eq_zero {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) {m n : ℕ} (hmn : m ≠ n) :
  ∫ (x : ℝ),
      Polynomial.eval x (Polynomial.jacobi α β m) *
        Polynomial.eval x (Polynomial.jacobi α β n) ∂Polynomial.jacobiMeasure α β =
    0

Lean proof

/-- Distinct Jacobi polynomials are orthogonal (DLMF Table 18.3.1). -/
theorem integral_mul_jacobi_eq_zero {α β : ℝ} (hα : -1 < α) (hβ : -1 < β)
    {m n : ℕ} (hmn : m ≠ n) :
    ∫ x, (jacobi α β m).eval x * (jacobi α β n).eval x ∂jacobiMeasure α β = 0 := by
  let c : ℝ := (n : ℝ) * (n + α + β + 1) - (m : ℝ) * (m + α + β + 1)
  have hint := integrable_jacobiMeasure hα hβ
    ((jacobi α β m).continuous.mul (jacobi α β n).continuous).continuousOn
  have hw := (integrable_jacobiMeasure_iff _ _ _).mp hint
  have hi := integral_eq_zero_of_hasDerivAt_jacobiWeight_mul hα hβ
    (((jacobi α β m).derivative.continuous.mul (jacobi α β n).continuous).sub
      ((jacobi α β m).continuous.mul (jacobi α β n).derivative.continuous)).continuousOn
    (jacobi_wronskian_hasDerivAt α β m n)
    (by convert hw.const_mul c using 1; ext x; dsimp [c]; ring)
  have hc : c ≠ 0 := by
    have hnm : (n : ℝ) ≠ m := by exact_mod_cast hmn.symm
    have hs : 1 ≤ n + m := by omega
    have hs' : (1 : ℝ) ≤ (n : ℝ) + m := by exact_mod_cast hs
    have hf : c = ((n : ℝ) - m) * ((n : ℝ) + m + α + β + 1) := by dsimp [c]; ring
    rw [hf]
    exact mul_ne_zero (sub_ne_zero.mpr hnm) (ne_of_gt (by linarith))
  rw [integral_jacobiMeasure α β
    ⟨fun x ↦ (jacobi α β m).eval (x : ℝ) * (jacobi α β n).eval (x : ℝ), hint⟩]
  apply (mul_eq_zero.mp (show c * (∫ x : Ioo (-1 : ℝ) 1,
      (jacobiWeight α β x : ℝ) * ((jacobi α β m).eval (x : ℝ) * (jacobi α β n).eval (x : ℝ))) = 0 from ?_)).resolve_left hc
  rw [← integral_const_mul]
  convert hi using 1
  congr 1
  funext x
  dsimp [c]
  ring

1 related Lean declaration

theorem Polynomial.isOrthogonal_jacobiSequence {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  (Polynomial.jacobiSequence hα hβ).IsOrthogonal (Polynomial.jacobiMeasure α β)

Lean proof

/-- The Jacobi sequence satisfies the general orthogonality predicate (DLMF Table 18.3.1). -/
theorem isOrthogonal_jacobiSequence {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
    (jacobiSequence hα hβ).IsOrthogonal (jacobiMeasure α β) where
  integrable _ _ := (hasFiniteMoments_jacobiMeasure hα hβ).integrable_mul _ _
  orthogonal _ _ hmn := integral_mul_jacobi_eq_zero hα hβ hmn

Write \(h_n=\int (P_n^{(\alpha ,\beta )})^2\, d\mu _{\alpha ,\beta }\) for the squared norm.

Theorem 3.2.24 Exact Jacobi squared norms

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\),

\[ h_0=\frac{2^{\alpha +\beta +1}\Gamma (\alpha +1)\Gamma (\beta +1)}{\Gamma (\alpha +\beta +2)}, \]

and for \(n\ge 1\),

\[ h_n=\frac{2^{\alpha +\beta +1}\Gamma (n+\alpha +1)\Gamma (n+\beta +1)}{(2n+\alpha +\beta +1)\Gamma (n+\alpha +\beta +1)n!}. \]

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integral_sq_jacobi_zero {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.jacobi α β 0) ^ 2 ∂Polynomial.jacobiMeasure α β =
    2 ^ (α + β + 1) * Real.GammaOn (Real.GammaPoint.ofPos (α + 1) ⋯) * Real.GammaOn (Real.GammaPoint.ofPos (β + 1) ⋯) /
      Real.GammaOn (Real.GammaPoint.ofPos (α + β + 2) ⋯)

Lean proof

/-- The classical Gamma formula; every displayed Gamma value excludes its poles. -/
theorem integral_sq_jacobi_zero {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
    ∫ x, (jacobi α β 0).eval x ^ 2 ∂jacobiMeasure α β =
      (2 : ℝ) ^ (α + β + 1) * GammaOn (GammaPoint.ofPos (α + 1) (by linarith)) * GammaOn (GammaPoint.ofPos (β + 1) (by linarith)) / GammaOn (GammaPoint.ofPos (α + β + 2) (by linarith)) :=
  integral_sq_jacobi_zero_gamma_formula hα hβ

1 related Lean declaration

theorem Polynomial.integral_sq_jacobi_succ {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.jacobi α β (n + 1)) ^ 2 ∂Polynomial.jacobiMeasure α β =
    2 ^ (α + β + 1) * Real.GammaOn (Real.GammaPoint.ofPos (↑n + α + 2) ⋯) *
        Real.GammaOn (Real.GammaPoint.ofPos (↑n + β + 2) ⋯) /
      ((2 * ↑n + α + β + 3) * Real.GammaOn (Real.GammaPoint.ofPos (↑n + α + β + 2) ⋯) * ↑(n + 1).factorial)

Lean proof

/-- The classical Gamma formula; every displayed Gamma value excludes its poles. -/
theorem integral_sq_jacobi_succ {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
    ∫ x, (jacobi α β (n + 1)).eval x ^ 2 ∂jacobiMeasure α β =
      (2 : ℝ) ^ (α + β + 1) * GammaOn (GammaPoint.ofPos (n + α + 2) (by have _hn : (0 : ℝ) ≤ n := Nat.cast_nonneg n; linarith)) * GammaOn (GammaPoint.ofPos (n + β + 2) (by have _hn : (0 : ℝ) ≤ n := Nat.cast_nonneg n; linarith)) /
        ((2 * n + α + β + 3) * GammaOn (GammaPoint.ofPos (n + α + β + 2) (by have _hn : (0 : ℝ) ≤ n := Nat.cast_nonneg n; linarith)) * (n + 1).factorial) :=
  integral_sq_jacobi_succ_gamma_formula hα hβ n

Theorem 3.2.25 Real simple Jacobi zeros

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\), \(P_n^{(\alpha ,\beta )}\) 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_jacobi {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) : (Polynomial.jacobi α β n).Splits

Lean proof

/-- Jacobi polynomials split over the reals (DLMF 18.2(vi)). -/
theorem splits_jacobi (n : ℕ) : (jacobi α β n).Splits :=
  (isOrthogonal_jacobiSequence hα hβ).splits (hasFiniteMoments_jacobiMeasure hα hβ)
    (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) n

2 related Lean declarations

theorem Polynomial.card_roots_jacobi {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) : (Polynomial.jacobi α β n).roots.card = n

Lean proof

/-- There are degree-many Jacobi roots (DLMF 18.2(vi)). -/
theorem card_roots_jacobi (n : ℕ) : (jacobi α β n).roots.card = n :=
  (isOrthogonal_jacobiSequence hα hβ).card_roots (hasFiniteMoments_jacobiMeasure hα hβ)
    (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) n

theorem Polynomial.separable_jacobi {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) : (Polynomial.jacobi α β n).Separable

Lean proof

/-- All Jacobi roots are simple (DLMF 18.2(vi)). -/
theorem separable_jacobi (n : ℕ) : (jacobi α β n).Separable :=
  (isOrthogonal_jacobiSequence hα hβ).separable (hasFiniteMoments_jacobiMeasure hα hβ)
    (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) n

Theorem 3.2.26 Jacobi root location

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\), \(P_n\) is orthogonal to every polynomial of degree below \(n\), and every real root of \(P_n\) lies in \((-1,1)\).

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

Lean Formalisation

theorem Polynomial.integral_mul_jacobi_eq_zero_of_degree_lt {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) {p : Polynomial ℝ} {n : ℕ}
  (hp : p.degree < ↑n) :
  ∫ (x : ℝ), Polynomial.eval x p * Polynomial.eval x (Polynomial.jacobi α β n) ∂Polynomial.jacobiMeasure α β = 0

Lean proof

/-- Orthogonality to every lower-degree polynomial (DLMF 18.2(i)). -/
theorem integral_mul_jacobi_eq_zero_of_degree_lt {p : ℝ[X]} {n : ℕ} (hp : p.degree < n) :
    ∫ x, p.eval x * (jacobi α β n).eval x ∂jacobiMeasure α β = 0 :=
  (isOrthogonal_jacobiSequence hα hβ).integralInner_eq_zero_of_degree_lt
    (hasFiniteMoments_jacobiMeasure hα hβ) hp

1 related Lean declaration

theorem Polynomial.root_jacobi_mem_Ioo {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) {n : ℕ} {x : ℝ}
  (hx : Polynomial.eval x (Polynomial.jacobi α β n) = 0) : x ∈ Set.Ioo (-1) 1

Lean proof

/-- Every Jacobi root lies strictly inside the orthogonality interval (DLMF 18.2(vi)). -/
theorem root_jacobi_mem_Ioo {n : ℕ} {x : ℝ} (hx : (jacobi α β n).eval x = 0) :
    x ∈ Ioo (-1) 1 := by
  have hl := neg_one_lt_root_jacobi hα hβ hx
  have hn : (jacobi β α n).eval (-x) = 0 := by rw [eval_jacobi_neg, hx, mul_zero]
  have hr := neg_one_lt_root_jacobi hβ hα hn
  exact ⟨hl, by linarith⟩

Theorem 3.2.27 Jacobi strict interlacing

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\), consecutive members have no common zero and mutually separate each other’s real zeros. For \(n\ge 1\), \(P_{n+1}\) has zeros \(a{\lt}b\) with every zero of \(P_n\) strictly between them.

Reference: [DLMF, 18.2(vi)].

Lean Formalisation

theorem Polynomial.not_eval_jacobi_eq_zero_and_succ {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) (x : ℝ) :
  ¬(Polynomial.eval x (Polynomial.jacobi α β n) = 0 ∧ Polynomial.eval x (Polynomial.jacobi α β (n + 1)) = 0)

Lean proof

/-- Consecutive members have no common root (DLMF 18.2(vi)). -/
theorem not_eval_jacobi_eq_zero_and_succ (n : ℕ) (x : ℝ) :
    ¬ ((jacobi α β n).eval x = 0 ∧ (jacobi α β (n + 1)).eval x = 0) :=
  (isOrthogonal_jacobiSequence hα hβ).not_eval_eq_zero_and_succ (hasFiniteMoments_jacobiMeasure hα hβ)
    (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) n x

3 related Lean declarations

theorem Polynomial.exists_root_jacobi_succ_between {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) {a b : ℝ} (hab : a < b)
  (ha : Polynomial.eval a (Polynomial.jacobi α β n) = 0) (hb : Polynomial.eval b (Polynomial.jacobi α β n) = 0) :
  ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.jacobi α β (n + 1)) = 0

Lean proof

/-- Between degree-n roots lies a degree-(n+1) root (DLMF 18.2(vi)). -/
theorem exists_root_jacobi_succ_between (n : ℕ) {a b : ℝ} (hab : a < b)
    (ha : (jacobi α β n).eval a = 0) (hb : (jacobi α β n).eval b = 0) :
    ∃ c ∈ Ioo a b, (jacobi α β (n + 1)).eval c = 0 :=
  (isOrthogonal_jacobiSequence hα hβ).exists_root_succ_between (hasFiniteMoments_jacobiMeasure hα hβ)
    (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) n hab ha hb

theorem Polynomial.exists_root_jacobi_between_succ {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) {a b : ℝ} (hab : a < b)
  (ha : Polynomial.eval a (Polynomial.jacobi α β (n + 1)) = 0)
  (hb : Polynomial.eval b (Polynomial.jacobi α β (n + 1)) = 0) :
  ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.jacobi α β n) = 0

Lean proof

/-- Between degree-(n+1) roots lies a degree-n root (DLMF 18.2(vi)). -/
theorem exists_root_jacobi_between_succ (n : ℕ) {a b : ℝ} (hab : a < b)
    (ha : (jacobi α β (n + 1)).eval a = 0) (hb : (jacobi α β (n + 1)).eval b = 0) :
    ∃ c ∈ Ioo a b, (jacobi α β n).eval c = 0 :=
  (isOrthogonal_jacobiSequence hα hβ).exists_root_between_succ (hasFiniteMoments_jacobiMeasure hα hβ)
    (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) n hab ha hb

theorem Polynomial.exists_outer_roots_jacobi {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) {n : ℕ} (hn : 1 ≤ n) :
  ∃ a b,
    a < b ∧
      Polynomial.eval a (Polynomial.jacobi α β (n + 1)) = 0 ∧
        Polynomial.eval b (Polynomial.jacobi α β (n + 1)) = 0 ∧
          ∀ (x : ℝ), Polynomial.eval x (Polynomial.jacobi α β n) = 0 → a < x ∧ x < b

Lean proof

/-- The higher-degree member has both outermost roots (DLMF 18.2(vi)). -/
theorem exists_outer_roots_jacobi {n : ℕ} (hn : 1 ≤ n) :
    ∃ a b : ℝ, a < b ∧ (jacobi α β (n + 1)).eval a = 0 ∧
      (jacobi α β (n + 1)).eval b = 0 ∧ ∀ x : ℝ, (jacobi α β n).eval x = 0 → a < x ∧ x < b :=
  (isOrthogonal_jacobiSequence hα hβ).exists_outer_roots (hasFiniteMoments_jacobiMeasure hα hβ)
    (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) hn

Weight properties and finite moments

Theorem 3.2.28 Jacobi weight positivity and support

✓ 🙂 human-reviewed

#

For all real \(\alpha ,\beta \), the weight \(w_{\alpha ,\beta }\) is measurable and strictly positive on its domain \((-1,1)\), and \(\mu _{\alpha ,\beta }\)-almost every point lies in \((-1,1)\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.measurable_jacobiWeight (α β : ℝ) : Measurable ⇑(Polynomial.jacobiWeight α β)

Lean proof

/-- The domain-typed Jacobi weight is measurable (DLMF Table 18.3.1). -/
theorem measurable_jacobiWeight (α β : ℝ) : Measurable (jacobiWeight α β) :=
  (jacobiWeight α β).continuous.measurable

3 related Lean declarations

theorem Polynomial.jacobiWeight_pos (α β : ℝ) (x : ↑(Set.Ioo (-1) 1)) : 0 < ↑((Polynomial.jacobiWeight α β) x)

Lean proof

/-- Strict positivity at every point of the classical domain (DLMF Table 18.3.1). -/
theorem jacobiWeight_pos (α β : ℝ) (x : Ioo (-1 : ℝ) 1) :
    0 < (jacobiWeight α β x : ℝ) :=
  jacobiWeight_pos_rpow α β x.property

theorem Polynomial.jacobiWeight_nonneg (α β : ℝ) (x : ↑(Set.Ioo (-1) 1)) : 0 ≤ ↑((Polynomial.jacobiWeight α β) x)

Lean proof

/-- Nonnegativity is part of the codomain, without any endpoint evaluation. -/
theorem jacobiWeight_nonneg (α β : ℝ) (x : Ioo (-1 : ℝ) 1) :
    0 ≤ (jacobiWeight α β x : ℝ) := (jacobiWeight α β x).property

theorem Polynomial.ae_mem_Ioo_jacobiMeasure (α β : ℝ) : ∀ᵐ (x : ℝ) ∂Polynomial.jacobiMeasure α β, x ∈ Set.Ioo (-1) 1

Lean proof

/-- The measure is concentrated on the open interval (DLMF Table 18.3.1). -/
theorem ae_mem_Ioo_jacobiMeasure (α β : ℝ) : ∀ᵐ x ∂jacobiMeasure α β, x ∈ Ioo (-1) 1 := by
  -- The measure is pushed forward from the open interval itself.
  rw [jacobiMeasure, openIntervalWeightMeasure]
  exact (ae_map_iff measurable_subtype_coe.aemeasurable
    (measurableSet_Ioo : MeasurableSet {x : ℝ | x ∈ Ioo (-1) 1})).2
    (Filter.Eventually.of_forall fun x ↦ x.property)

Theorem 3.2.29 Jacobi total mass

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\),

\[ \int _{-1}^1 w_{\alpha ,\beta }(x)\, dx=\int 1\, d\mu _{\alpha ,\beta } =\frac{2^{\alpha +\beta +1}\Gamma (\alpha +1)\Gamma (\beta +1)}{\Gamma (\alpha +\beta +2)}. \]

This is nonsingular also when \(\alpha +\beta +1=0\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.integral_jacobiWeight {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  ∫ (x : ↑(Set.Ioo (-1) 1)), ↑((Polynomial.jacobiWeight α β) x) =
    2 ^ (α + β + 1) * Real.GammaOn (Real.GammaPoint.ofPos (α + 1) ⋯) * Real.GammaOn (Real.GammaPoint.ofPos (β + 1) ⋯) /
      Real.GammaOn (Real.GammaPoint.ofPos (α + β + 2) ⋯)

Lean proof

/-- The classical Gamma formula; every displayed Gamma value excludes its poles. -/
theorem integral_jacobiWeight {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
    ∫ x : Ioo (-1 : ℝ) 1, (jacobiWeight α β x : ℝ) =
      (2 : ℝ) ^ (α + β + 1) * GammaOn (GammaPoint.ofPos (α + 1) (by linarith)) * GammaOn (GammaPoint.ofPos (β + 1) (by linarith)) / GammaOn (GammaPoint.ofPos (α + β + 2) (by linarith)) := by
  have h := integral_jacobiMeasure α β
    ⟨fun _ ↦ 1, integrable_jacobiMeasure hα hβ continuousOn_const⟩
  simp only [mul_one] at h
  exact h.symm.trans (integral_one_jacobiMeasure hα hβ)

1 related Lean declaration

theorem Polynomial.integral_one_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  ∫ (x : ℝ), 1 ∂Polynomial.jacobiMeasure α β =
    2 ^ (α + β + 1) * Real.GammaOn (Real.GammaPoint.ofPos (α + 1) ⋯) * Real.GammaOn (Real.GammaPoint.ofPos (β + 1) ⋯) /
      Real.GammaOn (Real.GammaPoint.ofPos (α + β + 2) ⋯)

Lean proof

/-- The classical Gamma formula; every displayed Gamma value excludes its poles. -/
theorem integral_one_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
    ∫ _ : ℝ, (1 : ℝ) ∂jacobiMeasure α β =
      (2 : ℝ) ^ (α + β + 1) * GammaOn (GammaPoint.ofPos (α + 1) (by linarith)) * GammaOn (GammaPoint.ofPos (β + 1) (by linarith)) / GammaOn (GammaPoint.ofPos (α + β + 2) (by linarith)) := by
  let aa : Complex.BetaParameter := ⟨((β+1 : ℝ) : ℂ), by simpa using (show 0 < β+1 by linarith)⟩
  let bb : Complex.BetaParameter := ⟨((α+1 : ℝ) : ℂ), by simpa using (show 0 < α+1 by linarith)⟩
  have hB : ((∫ t : Ioo (0 : ℝ) 1, (1-(t : ℝ))^α*(t : ℝ)^β : ℝ) : ℂ) =
      Complex.betaIntegralOn aa bb := by
    rw [← integral_complex_ofReal, Complex.betaIntegralOn]
    simp only [Measure.Subtype.volume_def]
    apply integral_congr_ae
    filter_upwards [] with t
    dsimp only [aa,bb]
    rw [Complex.ofReal_mul, Complex.ofReal_cpow (by linarith [t.property.2]),
      Complex.ofReal_cpow t.property.1.le]
    have h1 : (((β+1 : ℝ) : ℂ)-1) = (β : ℂ) := by push_cast; ring
    have h2 : (((α+1 : ℝ) : ℂ)-1) = (α : ℂ) := by push_cast; ring
    rw [h1,h2]
    push_cast
    ring
  have hG := Complex.betaIntegralOn_eq_Gamma aa bb
  change Complex.betaIntegralOn aa bb = Complex.Gamma ((β+1 : ℝ) : ℂ) *
    Complex.Gamma ((α+1 : ℝ) : ℂ) /
    Complex.Gamma (((β+1 : ℝ) : ℂ)+((α+1 : ℝ) : ℂ)) at hG
  have hs : (((β+1 : ℝ) : ℂ)+((α+1 : ℝ) : ℂ)) = ((α+β+2 : ℝ) : ℂ) := by push_cast; ring
  rw [hs,Complex.Gamma_ofReal,Complex.Gamma_ofReal,Complex.Gamma_ofReal] at hG
  have hR : (∫ t : Ioo (0 : ℝ) 1, (1-(t : ℝ))^α*(t : ℝ)^β) =
      Real.Gamma (β+1) * Real.Gamma (α+1) / Real.Gamma (α+β+2) := by
    apply Complex.ofReal_injective
    simpa only [Complex.ofReal_div,Complex.ofReal_mul] using hB.trans hG
  have hi : Integrable (fun _ : ℝ ↦ (1 : ℝ)) (unitJacobiMeasure α β) := by
    rw [unitJacobiMeasure, integrable_map_measure (by fun_prop) (by fun_prop)]
    exact integrable_jacobiMeasure hα hβ continuousOn_const
  have haff := integral_unitJacobiMeasure α β ⟨fun _ ↦ 1,hi⟩
  have hd := integral_unitJacobiMeasure_subtype α β ⟨fun _ ↦ 1,hi⟩ measurable_const
  simp only at haff hd
  simp only [mul_one] at hd
  rw [← haff,hd]
  simp_rw [unitJacobiWeight_apply]
  rw [integral_const_mul,hR]
  simp only [GammaOn, GammaPoint.ofPos]
  ring

3.2.4 Jacobi expansions

The integral coefficients retain the polynomial normalization used above. Every function in the weighted \(L^2\) space admits the resulting norm-convergent expansion.

Definition 3.2.30 Jacobi coefficients

✓ 🤖

#

For \(f\in \mathcal A_{\mu _{\alpha ,\beta },P_n^{(\alpha ,\beta )}}^{\mathbb {R}}\), define \(a_n(f)=h_n^{-1}\int fP_n\, d\mu _{\alpha ,\beta }\), where \(h_n=\int P_n^2\, d\mu _{\alpha ,\beta }\).

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

def Polynomial.jacobiCoefficient (α β : ℝ) {n : ℕ}
  (f : Polynomial.IntegralCoefficientInput ℝ (Polynomial.jacobiMeasure α β) (Polynomial.jacobi α β n)) : ℝ

Lean definition

/-- Jacobi integral coefficients on their full classical domain (DLMF 18.2(viii)). -/
@[expose] noncomputable def jacobiCoefficient (α β : ℝ) {n : ℕ}
    (f : IntegralCoefficientInput ℝ (jacobiMeasure α β) (jacobi α β n)) : ℝ :=
  (∫ x, (jacobi α β n).eval x ^ 2 ∂jacobiMeasure α β)⁻¹ *
    ∫ x, f.val x * (jacobi α β n).eval x ∂jacobiMeasure α β

1 related Lean declaration

def Polynomial.IntegralCoefficientInput.ofJacobiL2.{u_1} {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) {𝕂 : Type u_1} [RCLike 𝕂]
  (f : ↥(MeasureTheory.Lp 𝕂 2 (Polynomial.jacobiMeasure α β))) (n : ℕ) :
  Polynomial.IntegralCoefficientInput 𝕂 (Polynomial.jacobiMeasure α β) (Polynomial.jacobi α β n)

Lean definition

/-- L2 data in the classical Jacobi range supply every coefficient input
(DLMF 18.2(viii)). -/
@[expose] noncomputable def IntegralCoefficientInput.ofJacobiL2 {𝕂 : Type*} [RCLike 𝕂]
    (f : Lp 𝕂 2 (jacobiMeasure α β)) (n : ℕ) :
    IntegralCoefficientInput 𝕂 (jacobiMeasure α β) (jacobi α β n) :=
  IntegralCoefficientInput.ofL2 (hasFiniteMoments_jacobiMeasure hα hβ) (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ)
    (jacobi α β n) (by simpa only [jacobiSequence_apply] using (jacobiSequence hα hβ).ne_zero n) f

Theorem 3.2.31 Jacobi coefficient characterisation

✓ 🤖

#

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

Lean Formalisation

theorem Polynomial.jacobiCoefficient_apply (α β : ℝ) {n : ℕ}
  (f : Polynomial.IntegralCoefficientInput ℝ (Polynomial.jacobiMeasure α β) (Polynomial.jacobi α β n)) :
  Polynomial.jacobiCoefficient α β f =
    (∫ (x : ℝ), Polynomial.eval x (Polynomial.jacobi α β n) ^ 2 ∂Polynomial.jacobiMeasure α β)⁻¹ *
      ∫ (x : ℝ), f.val x * Polynomial.eval x (Polynomial.jacobi α β n) ∂Polynomial.jacobiMeasure α β

Lean proof

/-- The classical weighted formula includes its integrability and positive normalization. -/
theorem jacobiCoefficient_apply (α β : ℝ) {n : ℕ}
    (f : IntegralCoefficientInput ℝ (jacobiMeasure α β) (jacobi α β n)) :
    jacobiCoefficient α β f =
      (∫ x, (jacobi α β n).eval x ^ 2 ∂jacobiMeasure α β)⁻¹ *
        ∫ x, f.val x * (jacobi α β n).eval x ∂jacobiMeasure α β := rfl

The normalized polynomials are \(P_n^{(\alpha ,\beta )}/\sqrt{h_n}\), viewed as weighted \(L^2\) classes. The map \(J_\mu \) denotes polynomial evaluation followed by passage to this class (Definition 3.1.35).

Theorem 3.2.32 Jacobi completeness

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\), the normalised Jacobi polynomials form a Hilbert basis of real \(L^2(\mu _{\alpha ,\beta })\).

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

theorem Polynomial.polynomialToL2_jacobi_denseRange {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  DenseRange ⇑(Polynomial.polynomialToL2 ⋯)

Lean proof

/-- Jacobi polynomial classes are dense in weighted L² (DLMF 18.2(viii)). -/
theorem polynomialToL2_jacobi_denseRange :
    DenseRange (polynomialToL2 (hasFiniteMoments_jacobiMeasure hα hβ)) :=
  polynomialToL2_denseRange (hasFiniteMoments_jacobiMeasure hα hβ) (-1) 1
    ((ae_mem_Ioo_jacobiMeasure α β).mono (fun _ hx ↦ Set.Ioo_subset_Icc_self hx))

3 related Lean declarations

theorem Polynomial.orthonormal_normalizedJacobi {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  Orthonormal ℝ (Polynomial.normalizedJacobi hα hβ)

Lean proof

/-- The normalised Jacobi family is orthonormal (DLMF 18.2(viii)). -/
theorem orthonormal_normalizedJacobi : Orthonormal ℝ (normalizedJacobi hα hβ) :=
  (isOrthogonal_jacobiSequence hα hβ).orthonormal_normalizedToL2
    (hasFiniteMoments_jacobiMeasure hα hβ) (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ)

def Polynomial.hilbertBasisJacobi {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  HilbertBasis ℕ ℝ ↥(MeasureTheory.Lp ℝ 2 (Polynomial.jacobiMeasure α β))

Lean definition

/-- The Jacobi Hilbert basis (DLMF 18.2(viii)). -/
noncomputable def hilbertBasisJacobi : HilbertBasis ℕ ℝ (Lp ℝ 2 (jacobiMeasure α β)) :=
  (isOrthogonal_jacobiSequence hα hβ).hilbertBasis (hasFiniteMoments_jacobiMeasure hα hβ)
    (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) (polynomialToL2_jacobi_denseRange hα hβ)

theorem Polynomial.hilbertBasisJacobi_apply {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
  (Polynomial.hilbertBasisJacobi hα hβ) n = Polynomial.normalizedJacobi hα hβ n

Lean proof

/-- The Hilbert basis vectors are the normalised Jacobi classes (DLMF 18.2(viii)). -/
@[simp] theorem hilbertBasisJacobi_apply (n : ℕ) :
    hilbertBasisJacobi hα hβ n = normalizedJacobi hα hβ n :=
  (isOrthogonal_jacobiSequence hα hβ).hilbertBasis_apply (hasFiniteMoments_jacobiMeasure hα hβ)
    (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) (polynomialToL2_jacobi_denseRange hα hβ) n

Theorem 3.2.33 Jacobi L2 expansions

✓ 🤖

#

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

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

theorem Polynomial.hasSum_jacobiCoefficient_polynomialToL2 {α β : ℝ} (hα : -1 < α) (hβ : -1 < β)
  (f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.jacobiMeasure α β))) :
  HasSum
    (fun n =>
      Polynomial.jacobiCoefficient α β (Polynomial.IntegralCoefficientInput.ofJacobiL2 hα hβ f n) •
        (Polynomial.polynomialToL2 ⋯) (Polynomial.jacobi α β n))
    f

Lean proof

/-- Every weighted L² function is the sum of its Jacobi series in L² (DLMF 18.2(viii)). -/
theorem hasSum_jacobiCoefficient_polynomialToL2 (f : Lp ℝ 2 (jacobiMeasure α β)) :
    HasSum (fun n ↦ (jacobiCoefficient α β (IntegralCoefficientInput.ofJacobiL2 hα hβ f n)) •
      polynomialToL2 (hasFiniteMoments_jacobiMeasure hα hβ) (jacobi α β n)) f := by
  simpa only [Sequence.integralCoefficient, squaredNorm_jacobiSequence, jacobiSequence_apply,
    jacobiCoefficient, IntegralCoefficientInput.ofJacobiL2, IntegralCoefficientInput.ofL2] using
    (isOrthogonal_jacobiSequence hα hβ).hasSum_integralCoefficient
      (hasFiniteMoments_jacobiMeasure hα hβ) (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ)
      (polynomialToL2_jacobi_denseRange hα hβ) f

1 related Lean declaration

theorem Polynomial.tendsto_sum_jacobiCoefficient_polynomialToL2 {α β : ℝ} (hα : -1 < α) (hβ : -1 < β)
  (f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.jacobiMeasure α β))) :
  Filter.Tendsto
    (fun N =>
      ∑ n ∈ Finset.range N,
        Polynomial.jacobiCoefficient α β (Polynomial.IntegralCoefficientInput.ofJacobiL2 hα hβ f n) •
          (Polynomial.polynomialToL2 ⋯) (Polynomial.jacobi α β n))
    Filter.atTop (nhds f)

Lean proof

/-- Natural-order Jacobi partial sums converge in L² (DLMF 18.2(viii)). -/
theorem tendsto_sum_jacobiCoefficient_polynomialToL2 (f : Lp ℝ 2 (jacobiMeasure α β)) :
    Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.range N, (jacobiCoefficient α β (IntegralCoefficientInput.ofJacobiL2 hα hβ f n)) •
      polynomialToL2 (hasFiniteMoments_jacobiMeasure hα hβ) (jacobi α β n)) atTop (nhds f) :=
  (hasSum_jacobiCoefficient_polynomialToL2 hα hβ f).tendsto_sum_nat

Coefficient identification and weight calculus

Theorem 3.2.34 Jacobi coefficients as general coefficients

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\), the integral coefficients of the Jacobi sequence for \(\mu _{\alpha ,\beta }\) (Definition 3.1.38) are the Jacobi coefficients \(a_n(f)\), for \(f\in \mathcal A_{\mu _{\alpha ,\beta },P_n^{(\alpha ,\beta )}}^{\mathbb {R}}\).

Reference: [DLMF, 18.2(viii)].

Lean Formalisation

theorem Polynomial.integralCoefficient_jacobiSequence {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) {n : ℕ}
  (f : Polynomial.IntegralCoefficientInput ℝ (Polynomial.jacobiMeasure α β) (Polynomial.jacobi α β n)) :
  (Polynomial.jacobiSequence hα hβ).integralCoefficient (Polynomial.jacobiMeasure α β) f =
    Polynomial.jacobiCoefficient α β f

Lean proof

/-- The generic integral coefficients are the Jacobi coefficients on the
classical input domain (DLMF 18.2(viii)). -/
theorem integralCoefficient_jacobiSequence {n : ℕ}
    (f : IntegralCoefficientInput ℝ (jacobiMeasure α β) (jacobi α β n)) :
    (jacobiSequence hα hβ).integralCoefficient (jacobiMeasure α β) f =
      jacobiCoefficient α β f := by
  simp only [Sequence.integralCoefficient, squaredNorm_jacobiSequence,
    jacobiSequence_apply, jacobiCoefficient]

Theorem 3.2.35 Finite Jacobi moments

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\), \(\mu _{\alpha ,\beta }\) has finite polynomial moments and finite total mass.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.hasFiniteMoments_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  Polynomial.HasFiniteMoments (Polynomial.jacobiMeasure α β)

Lean proof

/-- Every polynomial square is integrable (DLMF Table 18.3.1). -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasFiniteMoments_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
    HasFiniteMoments (jacobiMeasure α β) := by
  intro p
  exact integrable_jacobiMeasure hα hβ (p.continuous.pow 2).continuousOn

1 related Lean declaration

theorem Polynomial.isFiniteMeasure_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  MeasureTheory.IsFiniteMeasure (Polynomial.jacobiMeasure α β)

Lean proof

/-- Finite total mass (DLMF Table 18.3.1). -/
theorem isFiniteMeasure_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
    IsFiniteMeasure (jacobiMeasure α β) :=
  (hasFiniteMoments_jacobiMeasure hα hβ).isFiniteMeasure

Theorem 3.2.36 Positive Jacobi pairing

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\) and \(p\ne 0\), \(\int p^2\, d\mu _{\alpha ,\beta }{\gt}0\).

Reference: [DLMF, 18.2(i)].

Lean Formalisation

theorem Polynomial.hasPositiveDefiniteIntegral_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  Polynomial.HasPositiveDefiniteIntegral (Polynomial.jacobiMeasure α β)

Lean proof

/-- Strict positivity of the polynomial pairing (DLMF 18.2(i), Table 18.3.1). -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasPositiveDefiniteIntegral_jacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
    HasPositiveDefiniteIntegral (jacobiMeasure α β) := by
  apply HasPositiveDefiniteIntegral.of_positive
  intro p hp
  have hex : ∃ x ∈ Ioo (-1 : ℝ) 1, p.eval x ≠ 0 := by
    by_contra h
    push Not at h
    exact hp (p.eq_zero_of_infinite_isRoot
      ((Ioo_infinite (show (-1 : ℝ) < 1 by norm_num)).mono h))
  have hi := integrable_jacobiMeasure hα hβ (p.continuous.pow 2).continuousOn
  rw [integral_jacobiMeasure α β ⟨fun x ↦ p.eval x ^ 2, hi⟩]
  have hi' := (integrable_jacobiMeasure_iff _ _ _).mp hi
  apply (integral_pos_iff_support_of_nonneg (fun x ↦
    mul_nonneg (jacobiWeight α β x).property (sq_nonneg _)) hi').2
  let : (volume : Measure (Ioo (-1 : ℝ) 1)).IsOpenPosMeasure :=
    Measure.IsOpenPosMeasure.comap volume isOpen_Ioo.isOpenEmbedding_subtypeVal
  have ho : IsOpen {x : Ioo (-1 : ℝ) 1 | p.eval (x : ℝ) ≠ 0} :=
    isOpen_ne.preimage (p.continuous.comp continuous_subtype_val)
  have hn : ({x : Ioo (-1 : ℝ) 1 | p.eval (x : ℝ) ≠ 0} : Set _).Nonempty := by
    obtain ⟨x, hx, hp⟩ := hex
    exact ⟨⟨x, hx⟩, hp⟩
  apply (ho.measure_pos volume hn).trans_le
  apply measure_mono
  intro x hx
  exact mul_ne_zero (jacobiWeight_pos α β x).ne' (pow_ne_zero _ hx)

Theorem 3.2.37 Jacobi polynomial sequence

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\), \(P_n^{(\alpha ,\beta )}\) has positive top coefficient and exact degree \(n\). These polynomials define a degree-indexed sequence.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

theorem Polynomial.coeff_jacobi_self_pos {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) : 0 < (Polynomial.jacobi α β n).coeff n

Lean proof

/-- The top coefficient is positive in the orthogonality range (DLMF Table 18.3.1). -/
theorem coeff_jacobi_self_pos {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
    0 < (jacobi α β n).coeff n := by
  rcases n with _ | n
  · simp
  rw [coeff_jacobi_self]
  apply mul_pos
  · positivity
  · apply ascPochhammer_pos
    push_cast
    linarith [Nat.cast_nonneg (α := ℝ) n]

3 related Lean declarations

theorem Polynomial.degree_jacobi_of_neg_one_lt {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
  (Polynomial.jacobi α β n).degree = ↑n

Lean proof

/-- Exact degree in the orthogonality range (DLMF Table 18.3.1). -/
theorem degree_jacobi_of_neg_one_lt {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
    (jacobi α β n).degree = n :=
  degree_eq_of_le_of_coeff_ne_zero (degree_jacobi_le α β n) (coeff_jacobi_self_pos hα hβ n).ne'

def Polynomial.jacobiSequence {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) : Polynomial.Sequence ℝ

Lean definition

/-- Jacobi polynomials as a degree-indexed sequence (DLMF Table 18.3.1). -/
@[expose] noncomputable def jacobiSequence {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) : Sequence ℝ where
  elems' := jacobi α β
  degree_eq' := degree_jacobi_of_neg_one_lt hα hβ

theorem Polynomial.jacobiSequence_apply {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
  ↑(Polynomial.jacobiSequence hα hβ) n = Polynomial.jacobi α β n

Lean proof

/-- The sequence uses the existing Jacobi polynomials (DLMF Table 18.3.1). -/
@[simp] theorem jacobiSequence_apply {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
    jacobiSequence hα hβ n = jacobi α β n := rfl

Definition 3.2.38 Continuous closed-interval Jacobi weight

✓ 🙂 human-reviewed

#

For \(\alpha ,\beta \ge 0\), define the continuous map \(\overline w_{\alpha ,\beta }:[-1,1]\to \mathbb {R}_{\ge 0}\) by \(\overline w_{\alpha ,\beta }(x)=(1-x)^\alpha (1+x)^\beta \), where \(0^0=1\).

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

def Polynomial.jacobiWeightClosed (α β : NNReal) : C(↑(Set.Icc (-1) 1), NNReal)

Lean definition

/-- The classical continuous extension for nonnegative exponents (DLMF 18.3.1). -/
@[expose] noncomputable def jacobiWeightClosed (α β : ℝ≥0) : C(Icc (-1 : ℝ) 1, ℝ≥0) where
  toFun x := ⟨(1 - (x : ℝ)) ^ (α : ℝ) * (1 + (x : ℝ)) ^ (β : ℝ),
    mul_nonneg (Real.rpow_nonneg (by linarith [x.property.2]) _)
      (Real.rpow_nonneg (by linarith [x.property.1]) _)⟩
  continuous_toFun := by
    apply Continuous.subtype_mk
    exact ((continuous_const.sub continuous_subtype_val).rpow_const (fun _ ↦ Or.inr α.property)).mul
      ((continuous_const.add continuous_subtype_val).rpow_const (fun _ ↦ Or.inr β.property))

Theorem 3.2.39 Closed Jacobi weight characterisation

✓ 🙂 human-reviewed

#

For \(\alpha ,\beta \ge 0\), the weight \(\overline w_{\alpha ,\beta }\) agrees with \(w_{\alpha ,\beta }\) on \((-1,1)\), and

\[ \overline w_{\alpha ,\beta }(1)=\begin{cases} 2^\beta & \alpha =0,\\ 0& \alpha {\gt}0,\end{cases} \qquad \overline w_{\alpha ,\beta }(-1)=\begin{cases} 2^\alpha & \beta =0,\\ 0& \beta {\gt}0.\end{cases} \]

Lean Formalisation

theorem Polynomial.jacobiWeightClosed_restrict (α β : NNReal) (x : ↑(Set.Ioo (-1) 1)) :
  ↑((Polynomial.jacobiWeightClosed α β) ⟨↑x, ⋯⟩) = ↑((Polynomial.jacobiWeight ↑α ↑β) x)

Lean proof

/-- The closed extension agrees with the original weight on its open domain. -/
theorem jacobiWeightClosed_restrict (α β : ℝ≥0) (x : Ioo (-1 : ℝ) 1) :
    (jacobiWeightClosed α β ⟨x, Ioo_subset_Icc_self x.property⟩ : ℝ) =
      (jacobiWeight α β x : ℝ) := rfl

2 related Lean declarations

theorem Polynomial.jacobiWeightClosed_one (α β : NNReal) :
  ↑((Polynomial.jacobiWeightClosed α β) ⟨1, Polynomial.jacobiWeightClosed_one._proof_1⟩) = if α = 0 then 2 ^ ↑β else 0

Lean proof

/-- The right endpoint value of the regular continuous extension. -/
theorem jacobiWeightClosed_one (α β : ℝ≥0) :
    (jacobiWeightClosed α β ⟨1, by constructor <;> norm_num⟩ : ℝ) =
      if α = 0 then (2 : ℝ) ^ (β : ℝ) else 0 := by
  by_cases h : α = 0
  · subst α
    norm_num [jacobiWeightClosed_apply]
  · have hr : (α : ℝ) ≠ 0 := by exact_mod_cast h
    simp [jacobiWeightClosed_apply, h, Real.zero_rpow hr]

theorem Polynomial.jacobiWeightClosed_neg_one (α β : NNReal) :
  ↑((Polynomial.jacobiWeightClosed α β) ⟨-1, Polynomial.jacobiWeightClosed_neg_one._proof_1⟩) =
    if β = 0 then 2 ^ ↑α else 0

Lean proof

/-- The left endpoint value of the regular continuous extension. -/
theorem jacobiWeightClosed_neg_one (α β : ℝ≥0) :
    (jacobiWeightClosed α β ⟨-1, by constructor <;> norm_num⟩ : ℝ) =
      if β = 0 then (2 : ℝ) ^ (α : ℝ) else 0 := by
  by_cases h : β = 0
  · subst β
    norm_num [jacobiWeightClosed_apply]
  · have hr : (β : ℝ) ≠ 0 := by exact_mod_cast h
    simp [jacobiWeightClosed_apply, h, Real.zero_rpow hr]

Theorem 3.2.40 Jacobi weight calculus

✓ 🙂 human-reviewed

#

On \((-1,1)\), for arbitrary real \(\alpha ,\beta \),

\[ w_{\alpha +1,\beta +1}=(1-x^2)w_{\alpha ,\beta },\qquad w_{\alpha +1,\beta +1}'=[\beta -\alpha -(\alpha +\beta +2)x]w_{\alpha ,\beta }. \]

If \(\alpha {\gt}-1\), the right endpoint limit of the shifted weight is zero, with no restriction on \(\beta \). If \(\beta {\gt}-1\), its left endpoint limit is zero, with no restriction on \(\alpha \).

Reference: [DLMF, Tables 18.3.1 and 18.8.1].

Lean Formalisation

theorem Polynomial.jacobiWeight_add_one (α β : ℝ) (x : ↑(Set.Ioo (-1) 1)) :
  ↑((Polynomial.jacobiWeight (α + 1) (β + 1)) x) = (1 - ↑x ^ 2) * ↑((Polynomial.jacobiWeight α β) x)

Lean proof

/-- Multiplying by `1-x²` shifts both parameters on the classical domain. -/
theorem jacobiWeight_add_one (α β : ℝ) (x : Ioo (-1 : ℝ) 1) :
    (jacobiWeight (α + 1) (β + 1) x : ℝ) =
      (1 - (x : ℝ) ^ 2) * (jacobiWeight α β x : ℝ) :=
  jacobiWeight_add_one_rpow α β x.property

3 related Lean declarations

theorem Polynomial.hasDerivAt_jacobiWeight_add_one (α β : ℝ) (x : ↑(Set.Ioo (-1) 1)) :
  HasDerivAtOnOpen { carrier := Set.Ioo (-1) 1, is_open' := ⋯ }
    (fun y => ↑((Polynomial.jacobiWeight (α + 1) (β + 1)) y))
    ((β - α - (α + β + 2) * ↑x) * ↑((Polynomial.jacobiWeight α β) x)) x

Lean proof

/-- The Pearson identity is an actual derivative of the open-domain weight. -/
theorem hasDerivAt_jacobiWeight_add_one (α β : ℝ) (x : Ioo (-1 : ℝ) 1) :
    HasDerivAtOnOpen ⟨Ioo (-1 : ℝ) 1, isOpen_Ioo⟩
      (fun y ↦ (jacobiWeight (α + 1) (β + 1) y : ℝ))
      ((β - α - (α + β + 2) * (x : ℝ)) * (jacobiWeight α β x : ℝ)) x := by
  classical
  -- Extend by zero off the interval; only the germ at the interior point `x`, where both
  -- power bases are positive, enters the derivative.
  refine ⟨fun t ↦ if h : t ∈ Ioo (-1 : ℝ) 1 then (jacobiWeight (α + 1) (β + 1) ⟨t, h⟩ : ℝ)
    else 0, fun y ↦ by simp, ?_⟩
  have hev : (fun t ↦ (1 - t) ^ (α + 1) * (1 + t) ^ (β + 1)) =ᶠ[𝓝 (x : ℝ)]
      fun t ↦ if h : t ∈ Ioo (-1 : ℝ) 1 then (jacobiWeight (α + 1) (β + 1) ⟨t, h⟩ : ℝ)
        else 0 := by
    filter_upwards [isOpen_Ioo.mem_nhds x.property] with t ht
    simp [ht, jacobiWeight_apply]
  exact (hasDerivAt_jacobiWeight_add_one_rpow α β x.property).congr_of_eventuallyEq hev.symm

theorem Polynomial.tendsto_jacobiWeight_add_one_one {α β : ℝ} (hα : -1 < α) :
  Filter.Tendsto (fun x => ↑((Polynomial.jacobiWeight (α + 1) (β + 1)) x)) (Filter.comap Subtype.val (nhds 1)) (nhds 0)

Lean proof

/-- The right endpoint limit exists with no condition on the opposite exponent. -/
theorem tendsto_jacobiWeight_add_one_one {α β : ℝ} (hα : -1 < α) :
    Tendsto (fun x : Ioo (-1 : ℝ) 1 ↦ (jacobiWeight (α + 1) (β + 1) x : ℝ))
      (Filter.comap Subtype.val (𝓝 (1 : ℝ))) (𝓝 0) := by
  have hval : Tendsto (Subtype.val : Ioo (-1 : ℝ) 1 → ℝ)
      (Filter.comap Subtype.val (𝓝 1)) (𝓝 1) := Filter.tendsto_comap
  -- The vanishing base is a nonnegative real, so its power is taken in `ℝ≥0`.
  let u : Ioo (-1 : ℝ) 1 → ℝ≥0 := fun x ↦ ⟨1 - (x : ℝ), by linarith [x.property.2]⟩
  have hu : Tendsto u (Filter.comap Subtype.val (𝓝 1)) (𝓝 0) := by
    rw [← NNReal.tendsto_coe]
    have h := (tendsto_const_nhds (x := (1 : ℝ))).sub hval
    rw [sub_self] at h
    exact h
  have h1 : Tendsto (fun x : Ioo (-1 : ℝ) 1 ↦ (1 - (x : ℝ)) ^ (α + 1))
      (Filter.comap Subtype.val (𝓝 1)) (𝓝 0) := by
    have h := ((NNReal.continuous_rpow_const (by linarith : (0 : ℝ) ≤ α + 1)).tendsto 0).comp hu
    rw [NNReal.zero_rpow (by linarith : α + 1 ≠ 0)] at h
    exact NNReal.tendsto_coe.mpr h
  -- The other base tends to `2`, so it stays positive near the endpoint.
  have h2 : Tendsto (fun x : Ioo (-1 : ℝ) 1 ↦ (1 + (x : ℝ)) ^ (β + 1))
      (Filter.comap Subtype.val (𝓝 1)) (𝓝 ((1 + 1) ^ (β + 1))) :=
    ((continuousAt_const.add continuousAt_id).rpow_const (Or.inl (by norm_num))).tendsto.comp hval
  have h := h1.mul h2
  rw [zero_mul] at h
  exact h

theorem Polynomial.tendsto_jacobiWeight_add_one_neg_one {α β : ℝ} (hβ : -1 < β) :
  Filter.Tendsto (fun x => ↑((Polynomial.jacobiWeight (α + 1) (β + 1)) x)) (Filter.comap Subtype.val (nhds (-1)))
    (nhds 0)

Lean proof

/-- The left endpoint limit exists with no condition on the opposite exponent. -/
theorem tendsto_jacobiWeight_add_one_neg_one {α β : ℝ} (hβ : -1 < β) :
    Tendsto (fun x : Ioo (-1 : ℝ) 1 ↦ (jacobiWeight (α + 1) (β + 1) x : ℝ))
      (Filter.comap Subtype.val (𝓝 (-1 : ℝ))) (𝓝 0) := by
  have hval : Tendsto (Subtype.val : Ioo (-1 : ℝ) 1 → ℝ)
      (Filter.comap Subtype.val (𝓝 (-1))) (𝓝 (-1)) := Filter.tendsto_comap
  -- The vanishing base is a nonnegative real, so its power is taken in `ℝ≥0`.
  let v : Ioo (-1 : ℝ) 1 → ℝ≥0 := fun x ↦ ⟨1 + (x : ℝ), by linarith [x.property.1]⟩
  have hv : Tendsto v (Filter.comap Subtype.val (𝓝 (-1))) (𝓝 0) := by
    rw [← NNReal.tendsto_coe]
    have h := (tendsto_const_nhds (x := (1 : ℝ))).add hval
    rw [add_neg_cancel] at h
    exact h
  have h2 : Tendsto (fun x : Ioo (-1 : ℝ) 1 ↦ (1 + (x : ℝ)) ^ (β + 1))
      (Filter.comap Subtype.val (𝓝 (-1))) (𝓝 0) := by
    have h := ((NNReal.continuous_rpow_const (by linarith : (0 : ℝ) ≤ β + 1)).tendsto 0).comp hv
    rw [NNReal.zero_rpow (by linarith : β + 1 ≠ 0)] at h
    exact NNReal.tendsto_coe.mpr h
  -- The other base tends to `2`, so it stays positive near the endpoint.
  have h1 : Tendsto (fun x : Ioo (-1 : ℝ) 1 ↦ (1 - (x : ℝ)) ^ (α + 1))
      (Filter.comap Subtype.val (𝓝 (-1))) (𝓝 ((1 - -1) ^ (α + 1))) :=
    ((continuousAt_const.sub continuousAt_id).rpow_const (Or.inl (by norm_num))).tendsto.comp hval
  have h := h1.mul h2
  rw [mul_zero] at h
  exact h

Theorem 3.2.41 Jacobi energy and norm shift

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\), set \(h_n^{(\alpha ,\beta )}=\int (P_n^{(\alpha ,\beta )})^2\, d\mu _{\alpha ,\beta }\). Then

\[ \int ((P_n^{(\alpha ,\beta )})')^2\, d\mu _{\alpha +1,\beta +1} =n(n+\alpha +\beta +1)h_n^{(\alpha ,\beta )}, \]

\[ h_{n+1}^{(\alpha ,\beta )}=\frac{n+\alpha +\beta +2}{4(n+1)}h_n^{(\alpha +1,\beta +1)}. \]

Reference: [DLMF, 18.9.15, Tables 18.3.1 and 18.8.1].

Lean Formalisation

theorem Polynomial.integral_sq_derivative_jacobi {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
  ∫ (x : ℝ),
      Polynomial.eval x (Polynomial.derivative (Polynomial.jacobi α β n)) ^
        2 ∂Polynomial.jacobiMeasure (α + 1) (β + 1) =
    ↑n * (↑n + α + β + 1) * ∫ (x : ℝ), Polynomial.eval x (Polynomial.jacobi α β n) ^ 2 ∂Polynomial.jacobiMeasure α β

Lean proof

/-- The Jacobi energy identity (DLMF Tables 18.3.1 and 18.8.1). -/
theorem integral_sq_derivative_jacobi {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
    ∫ x, (jacobi α β n).derivative.eval x ^ 2 ∂jacobiMeasure (α + 1) (β + 1) =
      ((n : ℝ) * (n + α + β + 1)) *
        ∫ x, (jacobi α β n).eval x ^ 2 ∂jacobiMeasure α β := by
  have hi0 := integrable_jacobiMeasure hα hβ
    ((jacobi α β n).continuous.pow 2).continuousOn
  have hi1 := integrable_jacobiMeasure (by linarith : -1 < α + 1)
    (by linarith : -1 < β + 1) ((jacobi α β n).derivative.continuous.pow 2).continuousOn
  have hw0 := (integrable_jacobiMeasure_iff _ _ _).mp hi0
  have hw1 := (integrable_jacobiMeasure_iff _ _ _).mp hi1
  simp only [Pi.pow_apply] at hw0 hw1
  have hi := integral_eq_zero_of_hasDerivAt_jacobiWeight_mul hα hβ
    ((jacobi α β n).derivative.continuous.mul (jacobi α β n).continuous).continuousOn
    (jacobi_energy_hasDerivAt α β n)
    (hw1.sub (hw0.const_mul ((n : ℝ) * (n + α + β + 1))))
  rw [integral_sub hw1 (hw0.const_mul _), integral_const_mul] at hi
  rw [integral_jacobiMeasure (α + 1) (β + 1)
    ⟨fun x ↦ (jacobi α β n).derivative.eval (x : ℝ) ^ 2, hi1⟩,
    integral_jacobiMeasure α β ⟨fun x ↦ (jacobi α β n).eval (x : ℝ) ^ 2, hi0⟩]
  exact sub_eq_zero.mp hi

1 related Lean declaration

theorem Polynomial.integral_sq_jacobi_succ_shift {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.jacobi α β (n + 1)) ^ 2 ∂Polynomial.jacobiMeasure α β =
    (↑n + α + β + 2) / (4 * (↑n + 1)) *
      ∫ (x : ℝ), Polynomial.eval x (Polynomial.jacobi (α + 1) (β + 1) n) ^ 2 ∂Polynomial.jacobiMeasure (α + 1) (β + 1)

Lean proof

/-- Lower the degree and raise both parameters in the squared norm
(DLMF 18.9.15 and Table 18.3.1). -/
theorem integral_sq_jacobi_succ_shift {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
    (∫ x, (jacobi α β (n + 1)).eval x ^ 2 ∂jacobiMeasure α β) =
      ((n : ℝ) + α + β + 2) / (4 * (n + 1)) *
        ∫ x, (jacobi (α + 1) (β + 1) n).eval x ^ 2 ∂jacobiMeasure (α + 1) (β + 1) := by
  have he := integral_sq_derivative_jacobi hα hβ (n + 1)
  have hd (x : ℝ) : (jacobi α β (n + 1)).derivative.eval (x : ℝ) =
      (((n : ℝ) + α + β + 2) / 2) * (jacobi (α + 1) (β + 1) n).eval (x : ℝ) := by
    rw [derivative_jacobi_succ, eval_mul, eval_C]
    norm_num [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
  simp_rw [hd, mul_pow] at he
  rw [integral_const_mul] at he
  have hc : 0 < (n : ℝ) + α + β + 2 := by linarith [Nat.cast_nonneg (α := ℝ) n]
  have hn : 0 < (n + 1 : ℝ) := by positivity
  apply mul_left_cancel₀ (mul_ne_zero hn.ne' hc.ne')
  calc
    _ = ((((n : ℝ) + α + β + 2) / 2) ^ 2) *
        ∫ x, (jacobi (α + 1) (β + 1) n).eval (x : ℝ) ^ 2 ∂jacobiMeasure (α + 1) (β + 1) := by
      convert he.symm using 1
      push_cast
      ring
    _ = _ := by field_simp; ring

Definition 3.2.42 Normalised Jacobi classes

✓ 🤖

#

For \(\alpha ,\beta {\gt}-1\), set \(e_n=h_n^{-1/2}J_{\mu _{\alpha ,\beta }}P_n^{(\alpha ,\beta )}\), where \(h_n\) is the squared integral norm.

Reference: [DLMF, Table 18.3.1].

Lean Formalisation

def Polynomial.normalizedJacobi {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
  ↥(MeasureTheory.Lp ℝ 2 (Polynomial.jacobiMeasure α β))

Lean definition

/-- Normalised Jacobi classes (DLMF Table 18.3.1). -/
noncomputable def normalizedJacobi (n : ℕ) : Lp ℝ 2 (jacobiMeasure α β) :=
  (jacobiSequence hα hβ).normalizedToL2 (hasFiniteMoments_jacobiMeasure hα hβ) ⟨n, Sequence.squaredNorm_pos (hasPositiveDefiniteIntegral_jacobiMeasure hα hβ) (jacobiSequence hα hβ) n⟩