sum_mul_smul — Mathlib

English

The canonical coercion from the Grassmannian to Submodule is definable; each W ∈ G(k,M;R) corresponds to its underlying submodule.

Русский

Каноническое включение из пространства Грассмана в Submodule задаётся однозначно; каждый элемент W соответствует своему базовому подпространству.

LaTeX

$$$\\text{toSubmodule}: \\mathrm{G}(k,M;R) \\to \\mathrm{Submodule}_R(M)$$$

Lean4

theorem sum_mul_smul (n : ℕ) :
    (∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν) = (n * (n - 1)) • X ^ 2 := by
  -- We calculate the second `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 second `x`-derivative, evaluate at `x=X, y=1-X`, and multiply by `X`:

  trans
    MvPolynomial.aeval e (pderiv true (pderiv true ((x + y) ^ n))) *
      X ^
        2
          -- On the left-hand side we'll use the binomial theorem, then simplify.

  · -- We first prepare a tedious rewrite:

    have w :
      ∀ k : ℕ,
        (k * (k - 1)) • bernsteinPolynomial R n k =
          (n.choose k : R[X]) *
              ((1 - Polynomial.X) ^ (n - k) * ((k : R[X]) * ((↑(k - 1) : R[X]) * Polynomial.X ^ (k - 1 - 1)))) *
            Polynomial.X ^ 2 :=
      by
      rintro (_ | _ | k)
      · simp
      · 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 (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, zero_add, mul_zero, smul_zero, mul_one, MvPolynomial.aeval_X, Derivation.leibniz_pow,
      Derivation.leibniz, Derivation.map_natCast, map_natCast, map_pow, map_mul]
      -- On the right-hand side, we'll just simplify.

  ·
    simp only [x, y, e, (pderiv _).leibniz_pow, (pderiv true).map_add, pderiv_true_x, pderiv_true_y,
      Algebra.id.smul_eq_mul, add_zero, mul_one, map_nsmul, map_pow, map_add, Bool.cond_true, Bool.cond_false,
      MvPolynomial.aeval_X, add_sub_cancel, one_pow, smul_smul, smul_one_mul]

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