fwdDiff_iter_eq_zero_of_degree_lt

English

If a polynomial P has natDegree < n, then Δ_1^[n] P.eval = 0.

Русский

Если натур_degree многочлена P меньше n, то Δ_1^[n] P.eval = 0.

LaTeX

$$$ \Delta_1^{[n]} P.eval = 0 $$$

Lean4

theorem fwdDiff_iter_eq_zero_of_degree_lt {P : R[X]} {n : ℕ} (hP : P.natDegree < n) : Δ_[1]^[n] P.eval = 0 :=
  funext fun x ↦ by
    obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_lt hP
    rw [add_assoc, add_comm, Function.iterate_add_apply, Function.iterate_succ_apply,
      P.fwdDiff_iter_degree_eq_factorial, Pi.smul_def]
    simp [fwdDiff_iter_eq_sum_shift]

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