sum — Mathlib

English

For any commutative ring R and any n ∈ ℕ, the sum of Bernstein polynomials B_{n,ν} over ν=0,...,n equals the constant polynomial 1.

Русский

Пусть R — коммутативное кольцо. Для любого n ∈ ℕ сумма Bernstein-полиномов B_{n,ν} по ν=0,...,n равна константному полиномy 1.

LaTeX

$$$ \sum_{\nu=0}^{n} bernsteinPolynomial R n ν = 1 $$$

Lean4

theorem sum (n : ℕ) : (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν) = 1 :=
  calc
    (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν) = (X + (1 - X)) ^ n :=
      by
      rw [add_pow]
      simp only [bernsteinPolynomial, mul_comm, mul_assoc]
    _ = 1 := by simp

Похожие утверждения