linearIndependent_aux — Mathlib

English

For natural numbers n and k with k ≤ n+1, the collection {bernsteinPolynomial ℚ n ν} for ν in 0,...,k−1 is linearly independent over ℚ.

Русский

Для натуральных чисел n и k с k ≤ n+1 множество {bernsteinPolynomial ℚ n ν} для ν=0,...,k−1 линейно независимо над ℚ.

LaTeX

$$$ LinearIndependent\, \mathbb{Q} \; (\nu : Fin k) \mapsto bernsteinPolynomial \mathbb{Q} n \nu $$$

Lean4

theorem linearIndependent_aux (n k : ℕ) (h : k ≤ n + 1) :
    LinearIndependent ℚ fun ν : Fin k => bernsteinPolynomial ℚ n ν := by
  induction k with
  | zero => apply linearIndependent_empty_type
  | succ k ih =>
    apply linearIndependent_fin_succ'.mpr
    fconstructor
    · exact ih (le_of_lt h)
    · -- The actual work!
            -- We show that the (n-k)-th derivative at 1 doesn't vanish,
            -- but vanishes for everything in the span.

      clear ih
      simp only [add_le_add_iff_right] at h
      simp only [Fin.val_last, Fin.init_def]
      dsimp
      apply
        notMem_span_of_apply_notMem_span_image
          (@Polynomial.derivative ℚ _ ^ (n - k))
            -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `span_image` into `span_image _`

      simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image _]
      intro p m
      apply_fun Polynomial.eval (1 : ℚ)
      simp only [Module.End.pow_apply]
        -- The right-hand side is nonzero,
              -- so it will suffice to show the left-hand side is always zero.

      suffices (Polynomial.derivative^[n - k] p).eval 1 = 0
        by
        rw [this]
        exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
      refine span_induction ?_ ?_ ?_ ?_ m
      · simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
        rintro ⟨a, w⟩; simp only
        rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((tsub_lt_tsub_iff_left_of_le h).mpr w)]
      · simp
      · intro x y _ _ hx hy; simp [hx, hy]
      · intro a x _ h; simp [h]

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