English
For n with n ≠ 0, Bernstein.z(Fin.last n) = 1.
Русский
Для n, где n ≠ 0, Bernstein.z(Fin.last n) = 1.
LaTeX
$$$\operatorname{bernstein}.z(\mathrm{Fin}.last\ n) = 1 \quad (n \ne 0)$$$
Lean4
theorem variance {n : ℕ} (hn : n ≠ 0) (x : I) :
(∑ k : Fin (n + 1), (x - k/ₙ : ℝ) ^ 2 * bernstein n k x) = (x : ℝ) * (1 - x) / n :=
by
convert congr(Polynomial.aeval (x : ℝ) $(bernsteinPolynomial.variance ℝ n) / n ^ 2) using 1
· simp only [z, bernstein_apply, nsmul_eq_mul, bernsteinPolynomial, Finset.sum_range, map_sum,
Polynomial.coe_aeval_eq_eval, Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_sub,
Polynomial.eval_natCast, Polynomial.eval_X, Polynomial.eval_one]
field_simp
rw [← Finset.sum_div]
field_simp
· simp
field_simp
