Polynomial.hermite_succ
theorem Polynomial.hermite_succ :
∀ (n : ℕ),
Polynomial.hermite (n + 1) = Polynomial.X * Polynomial.hermite n - Polynomial.derivative (Polynomial.hermite n)
This theorem establishes a recursive relation for the Hermite polynomials, which are commonly used in probability theory. For any given natural number `n`, the `(n + 1)`th Hermite polynomial can be computed as the product of the polynomial variable `X` and the `n`th Hermite polynomial, subtracted by the derivative of the `n`th Hermite polynomial. Formally, this relationship can be expressed as `hermite (n+1) = X * hermite(n) - d/dx (hermite n)`.
More concisely: The Hermite polynomial of degree `n+1` is given recursively as `X * hermite(n) - d/dx (hermite n)`, where `X` is a polynomial variable and `hermite` denotes the Hermite polynomial function.
|
Polynomial.coeff_hermite_explicit
theorem Polynomial.coeff_hermite_explicit :
∀ (n k : ℕ),
(Polynomial.hermite (2 * n + k)).coeff k = (-1) ^ n * ↑(2 * n - 1).doubleFactorial * ↑((2 * n + k).choose k)
The theorem `Polynomial.coeff_hermite_explicit` states that for any nonnegative integer values of `n` and `k`, the `k`-th coefficient of the Hermite polynomial (which is defined by the probabilists' definition), indexed by `(2 * n + k)`, is given by the product of the (-1) raised to the power `n`, the double factorial of `(2 * n - 1)`, and the binomial coefficient of `(2 * n + k)` choose `k`. Essentially, when the Hermite polynomial's index is an odd number, this theorem describes every nonzero coefficient of the polynomial.
More concisely: For any nonnegative integer `n` and `k`, the `k`-th coefficient of the Hermite polynomial, indexed by `(2 * n + k)`, is given by the product of `(-1)^n`, the double factorial `(2 * n - 1)!`, and the binomial coefficient `binomial 2 * n k`.
|
Polynomial.coeff_hermite_of_lt
theorem Polynomial.coeff_hermite_of_lt : ∀ {n k : ℕ}, n < k → (Polynomial.hermite n).coeff k = 0
The theorem `Polynomial.coeff_hermite_of_lt` asserts that for any two natural numbers `n` and `k`, if `n` is less than `k`, then the coefficient of `X^k` in the Hermite polynomial of degree `n` is equal to zero. In other words, in the Hermite polynomial represented as a sum of terms with the form `a_i * X^i`, if `i` is greater than the polynomial's degree, then `a_i` is zero.
More concisely: For any natural numbers `n` and `k` with `n < k`, the coefficient of `X^k` in the Hermite polynomial of degree `n` is zero.
|
Polynomial.coeff_hermite_succ_succ
theorem Polynomial.coeff_hermite_succ_succ :
∀ (n k : ℕ),
(Polynomial.hermite (n + 1)).coeff (k + 1) =
(Polynomial.hermite n).coeff k - (↑k + 2) * (Polynomial.hermite n).coeff (k + 2)
The theorem `Polynomial.coeff_hermite_succ_succ` states that for all natural numbers `n` and `k`, the coefficient of the term `X^(k+1)` in the (n+1)-th Hermite polynomial equals the coefficient of the term `X^k` in the n-th Hermite polynomial minus the product of the real number `k+2` and the coefficient of the term `X^(k+2)` in the n-th Hermite polynomial. This essentially provides a recursive formula to calculate the coefficients of the terms in the Hermite polynomials.
More concisely: The coefficient of `X^(k+1)` in the (n+1)-th Hermite polynomial is equal to the coefficient of `X^k` in the n-th Hermite polynomial minus (k+2) times the coefficient of `X^(k+2)` in the n-th Hermite polynomial.
|