English
For a commutative ring R and natural n, the sum over ν from 0 to n of (nX − ν)^2 times the Bernstein polynomial B_n,ν equals nX(1 − X).
Русский
Для коммутативного кольца R и натурального n сумма по ν от 0 до n из (nX − ν)^2 умноженного на Bernstein B_n,ν равна nX(1 − X).
LaTeX
$$$\\sum_{\\nu=0}^n (n \\cdot X - \\nu)^2 \\cdot \\mathrm{bernsteinPolynomial}\\;R\\;n\\;\\nu = n \\cdot X \\cdot (1 - X)$$$
Lean4
/-- A certain linear combination of the previous three identities,
which we'll want later.
-/
theorem variance (n : ℕ) :
(∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - (ν : R[X])) ^ 2 * bernsteinPolynomial R n ν) =
n • Polynomial.X * ((1 : R[X]) - Polynomial.X) :=
by
have p :
((((Finset.range (n + 1)).sum fun ν => (ν * (ν - 1)) • bernsteinPolynomial R n ν) +
(1 - (2 * n) • Polynomial.X) * (Finset.range (n + 1)).sum fun ν => ν • bernsteinPolynomial R n ν) +
n ^ 2 • X ^ 2 * (Finset.range (n + 1)).sum fun ν => bernsteinPolynomial R n ν) =
_ :=
rfl
conv at p =>
lhs
rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
simp only [← natCast_mul]
simp only [← mul_assoc]
simp only [← add_mul]
conv at p =>
rhs
rw [sum, sum_smul, sum_mul_smul, ← natCast_mul]
calc
_ = _ := Finset.sum_congr rfl fun k m => ?_
_ = _ := p
_ = _ := ?_
· congr 1; simp only [← natCast_mul, push_cast]
cases k <;> · simp; ring
· simp only [← natCast_mul, push_cast]
cases n
· simp
· simp; ring
