n : ℕ
x : ↑I
this : ∑ ν in Finset.range (n + 1), bernsteinPolynomial ℝ n ν = 1
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
n : ℕ
x : ↑I
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
have := bernsteinPolynomial.sum ℝ n
n : ℕ
x : ↑I
this : ↑(Polynomial.aeval ↑x) (∑ ν in Finset.range (n + 1), bernsteinPolynomial ℝ n ν) = ↑(Polynomial.aeval ↑x) 1
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
n : ℕ
x : ↑I
this : ∑ ν in Finset.range (n + 1), bernsteinPolynomial ℝ n ν = 1
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
apply_fun fun p => Polynomial.aeval (x : ℝ) p at this
n : ℕ
x : ↑I
this : ∑ x_1 : Fin (n + 1), Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = 1
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
n : ℕ
x : ↑I
this : ↑(Polynomial.aeval ↑x) (∑ ν in Finset.range (n + 1), bernsteinPolynomial ℝ n ν) = ↑(Polynomial.aeval ↑x) 1
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
simp [AlgHom.map_sum, Finset.sum_range] at this
no goals
n : ℕ
x : ↑I
this : ∑ x_1 : Fin (n + 1), Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = 1
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
exact this