bernsteinPolynomial.variance
theorem bernsteinPolynomial.variance :
∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
((Finset.range (n + 1)).sum fun ν => (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial R n ν) =
n • Polynomial.X * (1 - Polynomial.X)
The theorem `bernsteinPolynomial.variance` states that for any commutative ring `R` and any natural number `n`, the sum of the square of `(n * Polynomial.X - ν)` times the Bernstein polynomial of `n` and `ν`, for all `ν` in the set of natural numbers less than `n + 1`, equals `n * Polynomial.X * (1 - Polynomial.X)`. In mathematical terms, this can be written as $\sum_{\nu=0}^{n} (nX - \nu)^{2} \cdot B_{n,\nu}(X) = nX(1 - X)$, where $B_{n,\nu}(X)$ is the Bernstein polynomial.
More concisely: For any commutative ring R and natural number n, the sum of the squares of the difference between nX and a natural number ν less than n+1, and the corresponding Bernstein polynomial Bn,ν(X), equals nX(1-X). In other words, ∑ₙ=0^(n-1) (nx-ν)² ⋅ Bn,ν(X) = nX(1-X).
|
bernsteinPolynomial.linearIndependent
theorem bernsteinPolynomial.linearIndependent : ∀ (n : ℕ), LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν := by
sorry
This theorem asserts that Bernstein polynomials are linearly independent. It is proven by induction for a collection of Bernstein polynomials `bernsteinPolynomial n ν` where `ν` ranges from 0 to `k`. The basis for the inductive step is the fact that the `(n-k)`-th derivative of a Bernstein polynomial, when evaluated at 1, nullifies `bernsteinPolynomial n ν` for `ν < k`, but obtains a non-zero value when `ν = k`. In other words, the lower order Bernstein polynomials have all their `(n-k)`-th derivatives at 1 equal to zero, making them linearly independent from the `k`-th order one, which has a non-zero `(n-k)`-th derivative at 1.
More concisely: The collection of Bernstein polynomials of order `n` with degrees ranging from `0` to `k` is linearly independent.
|