English
Let n,k be natural numbers with k ≤ n+1. The same auxiliary linear independence statement for the Bernstein polynomials over ℚ holds (as in the previous item).
Русский
Пусть n,k ∈ ℕ с k ≤ n+1. То же вспомогательное утверждение о линейной независимости Бернштейн-полиномов над ℚ верно.
LaTeX
$$$ LinearIndependent\, \mathbb{Q} (\nu : Fin k) \mapsto bernsteinPolynomial \mathbb{Q} n \nu $$$
Lean4
/-- The Bernstein polynomials are linearly independent.
We prove by induction that the collection of `bernsteinPolynomial n ν` for `ν = 0, ..., k`
are linearly independent.
The inductive step relies on the observation that the `(n-k)`-th derivative, evaluated at 1,
annihilates `bernsteinPolynomial n ν` for `ν < k`, but has a nonzero value at `ν = k`.
-/
theorem linearIndependent (n : ℕ) : LinearIndependent ℚ fun ν : Fin (n + 1) => bernsteinPolynomial ℚ n ν :=
linearIndependent_aux n (n + 1) le_rfl
