Supplement to the fwdDiff theorem in mathelib

Stream: mathlib4

[SHAO YU]

theorem diff_n_times_on_pow_k   {j n: ℕ } (h: j < n): Δ_[1] ^[n] (fun x ↦ x^j : ℕ → ℝ ) x = (fun _ ↦  (0:ℝ ) ) x := by
  revert j
  induction n with
  | zero => simp;
  | succ n ih =>
    intro j hj
    simp
    rw [fwdDiff_iter_eq_sum_shift]
    simp
    conv at ih=>
      simp
      intro j h2
      simp
      enter [1];rw [fwdDiff_iter_eq_sum_shift]
      simp
    have l2 (k:ℕ ):((x + k) ^ j ) ≤ ((x + k + 1) ^ j  ):=by
      apply Nat.pow_le_pow_of_le_left
      linarith
    conv_lhs=>enter[2];ext k;enter[2];simp;rw [fwdDiff,← cast_pow,← cast_pow,← cast_sub (by exact l2 k)]
    conv_lhs=>enter[2];ext k;enter[2,1,1];rw [add_pow,sum_range_succ];simp
    conv_lhs=>enter[2];ext k;enter[2,1];rw [Nat.add_sub_cancel_right (m:=(x+k)^j)]
    conv_lhs=>enter [2];ext k;rw [mul_assoc,← cast_mul,mul_sum]
    norm_num
    conv_lhs=>enter [2];ext k;rw [mul_sum]
    rw [sum_comm]
    conv_lhs=>enter[2];ext i;enter [2];ext k;rw [← mul_assoc,← mul_assoc]
    conv_lhs=>enter[2];ext i;rw [← sum_mul]
    apply Finset.sum_eq_zero
    intro i hi
    simp at hi
    have lt : i < n := by linarith
    simp
    left
    conv at ih=>
      simp
      intro j hj
      simp
    rw [ih]
    exact lt


theorem diff_n_times_on_pow_n  {n: ℕ } : Δ_[1] ^[n] (fun x ↦ x^n : ℕ → ℝ ) x = (fun _ ↦  (n.factorial:ℝ ) ) x := by
  --revert j
  induction n with
  | zero => simp;
  | succ n ih =>
    --intro j hj
    simp
    rw [fwdDiff_iter_eq_sum_shift]
    simp
    conv at ih=>
      simp
      simp
      enter [1];rw [fwdDiff_iter_eq_sum_shift]
      simp
    have l2 (k:ℕ ):((x + k) ^ (n+1) ) ≤ ((x + k + 1) ^ (n+1)  ):=by
      apply Nat.pow_le_pow_of_le_left
      linarith
    conv_lhs=>enter[2];ext k;enter[2];simp;rw [fwdDiff,← cast_pow,← cast_pow,← cast_sub (by exact l2 k)]
    conv_lhs=>enter[2];ext k;enter[2,1,1];rw [add_pow,sum_range_succ];simp
    conv_lhs=>enter[2];ext k;enter[2,1];rw [Nat.add_sub_cancel_right]
    conv_lhs=>enter [2];ext k;rw [mul_assoc,← cast_mul,mul_sum]
    norm_num
    conv_lhs=>enter [2];ext k;rw [mul_sum]
    rw [sum_comm]
    conv_lhs=>enter[2];ext i;enter [2];ext k;rw [← mul_assoc,← mul_assoc]
    conv_lhs=>enter[2];ext i;rw [← sum_mul]
    rw [sum_range_succ,ih]
    rw [Step2]
    simp
    norm_cast
    nth_rw 1 [show n =n+1-1 by rw [Nat.add_sub_cancel]]
    rw [mul_comm,Nat.mul_factorial_pred ]
    linarith

[Martin Dvořák]

Do you want us to refactor your code into the Mathlib style? Or what is the question?

[Yaël Dillies]

@Martin Dvořák, I just noticed that the code above is a formalisation of the question you asked in #Is there code for X? > Differences of powers @ 💬

[Martin Dvořák]

Where is Δ_[1] defined? What do we need to import to make your code work?
@SHAO YU

[Yaël Dillies]

It's docs#fwdDiff

[Damiano Testa]

When Yaël is not around, you can find out as follow:

import Mathlib

#find_syntax "Δ_"

#check fwdDiff.«termΔ_[_]»
-- import Mathlib.Algebra.Group.ForwardDiff