sum_smul — Mathlib

English

Let R be a commutative ring. The weighted sum with weights ν(ν−1) of Bernstein polynomials equals (n choose 2) times X^2, i.e., (n(n−1)) X^2 when appropriate linearly scaled.

Русский

Пусть R — коммутативное кольцо. Взвешенная сумма с весами ν(ν−1) для Bernstein-полиномов равна (n choose 2) X^2, то есть (n(n−1)) X^2 после соответствующего масштаба линейной комбинации.

LaTeX

$$$ \sum_{\nu=0}^{n} (\nu(\nu-1)) \cdot bernsteinPolynomial R n ν = (n(n-1)) \cdot X^2 $$$

Lean4

theorem sum_smul (n : ℕ) : (∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν) = n • X := by
  -- We calculate the `x`-derivative of `(x+y)^n`, evaluated at `y=(1-x)`,
    -- either directly or by using the binomial theorem.
    -- We'll work in `MvPolynomial Bool R`.

  let x : MvPolynomial Bool R := MvPolynomial.X true
  let y : MvPolynomial Bool R := MvPolynomial.X false
  have pderiv_true_x : pderiv true x = 1 := by rw [pderiv_X]; rfl
  have pderiv_true_y : pderiv true y = 0 := by rw [pderiv_X]; rfl
  let e : Bool → R[X] := fun i =>
    cond i X
      (1 - X)
        -- Start with `(x+y)^n = (x+y)^n`,
          -- take the `x`-derivative, evaluate at `x=X, y=1-X`, and multiply by `X`:

  trans MvPolynomial.aeval e (pderiv true ((x + y) ^ n)) * X
  · -- We first prepare a tedious rewrite:

    have w :
      ∀ k : ℕ,
        k • bernsteinPolynomial R n k =
          (k : R[X]) * Polynomial.X ^ (k - 1) * (1 - Polynomial.X) ^ (n - k) * (n.choose k : R[X]) * Polynomial.X :=
      by
      rintro (_ | k)
      · simp
      · rw [bernsteinPolynomial]
        simp only [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]
        push_cast
        ring
    rw [add_pow, map_sum (pderiv true), map_sum (MvPolynomial.aeval e), Finset.sum_mul]
      -- Step inside the sum:

    refine Finset.sum_congr rfl fun k _ => (w k).trans ?_
    simp only [x, y, e, pderiv_true_x, pderiv_true_y, Algebra.id.smul_eq_mul, nsmul_eq_mul, Bool.cond_true,
      Bool.cond_false, add_zero, mul_one, mul_zero, smul_zero, MvPolynomial.aeval_X, MvPolynomial.pderiv_mul,
      Derivation.leibniz_pow, Derivation.map_natCast, map_natCast, map_pow, map_mul]
  · rw [(pderiv true).leibniz_pow, (pderiv true).map_add, pderiv_true_x, pderiv_true_y]
    simp only [x, y, e, Algebra.id.smul_eq_mul, nsmul_eq_mul, map_natCast, map_pow, map_add, map_mul, Bool.cond_true,
      Bool.cond_false, MvPolynomial.aeval_X, add_sub_cancel, one_pow, add_zero, mul_one]

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