Def difference Operatorand and prove it's some equals?

Stream: mathlib4

[SHAO YU]

import Mathlib
import Mathlib.Tactic
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Int.Cast.Basic
import Mathlib.Data.Nat.Cast.Basic
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Algebra.GroupWithZero.Units.Lemmas
import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Data.Nat.Choose.Basic

open Nat
open Finset
open Polynomial

variable {R : Type v} [Ring R] {R2 : Type v} [Ring R2]
--def f (k j:ℕ ):ℤ → R:= k^j
def diff (f : ℤ → R) : ℤ → R := fun x => f (x + 1) - f (x)
--def f (k j:ℕ ):= k^j
#synth SMul R (ℤ → R)


def diff_linear_map : (ℤ → R) →ₗ[R] (ℤ → R) where
  toFun := diff
  map_add' := fun x y => by
    unfold diff; ext i; dsimp; abel
  map_smul' := fun a x => by
    unfold diff; ext i; dsimp; rw [mul_sub]

lemma comp_comm (f : R →+ R2) : (Function.comp f) ∘ (diff) = (diff) ∘ (Function.comp f) := by
  ext x y
  unfold diff
  simp


lemma comp_n_times_comm (n : ℕ) (f : R →+ R2) : (Function.comp f) ∘ (diff^[n]) = (diff^[n]) ∘ (Function.comp f) := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp only [Function.iterate_succ]
    rw [← Function.comp_assoc]
    rw [ih]
    rw [Function.comp_assoc]
    rw [comp_comm]
    rw [Function.comp_assoc]

def diff_nth_linear_map (n : ℕ) : (ℤ → R) →ₗ[R] (ℤ → R) :=
  match n with
  | Nat.zero => LinearMap.id
  | Nat.succ k => (diff_nth_linear_map k).comp diff_linear_map

theorem diff_nth_linear_map_eq (n : ℕ) (f : ℤ → R) :
  (diff_nth_linear_map n : (ℤ → R) →ₗ[R] (ℤ → R)) f = (diff^[n]) f := by
  induction n generalizing f with
  | zero => rfl
  | succ n ih =>
    unfold diff_nth_linear_map
    simp only [LinearMap.coe_comp, Function.comp_apply, Function.iterate_succ]
    rw [ih]; rfl



lemma l1 (k:ℕ )(hk:k>0) (f : ℤ → R): ∑ j in range (k+1+1),(-1:ℤ )^(k-j+1) * (k.choose (j-1):R ) * f (x+j)
  =0 + ∑ j in Ico 1 (k+1+1),(-1:ℤ )^(k-j+1) * k.choose (j-1) * f (x+j):=by
  rw [range_eq_Ico]




theorem diff_n_times_eq (n : ℕ) (f : ℤ → R):
    (diff^[n]) f = fun x => ∑ i in range (n+1), ((-1:ℤ)^(n-i) * (n.choose i) * f (x+i)) :=
  match n with
  | Nat.zero => by simp
  | Nat.succ k => by
    let diff_n_minus_1 := diff_n_times_eq k f
    rw [(Function.iterate_succ' _ _ : diff^[k+1] = diff ∘ (diff^[k])), Function.comp_apply]
    rw [diff_n_minus_1]
    ext x; dsimp [diff]

    --conv_lhs=>enter [1,2];ext i; rw [l1,l2];enter[2];rw [l3]
    have eq1: ∑ i ∈ Ico 0 (k + 1), (-1:ℤ ) ^ (k - i) * (k.choose i) * f (x + 1+↑i)=∑ i ∈ Ico 1 (k + 1+1), ↑(-1) ^ (k - i+1) * (k.choose (i-1)) * f (x +↑i):=by
      symm
      rw [← Finset.sum_Ico_add (c:=1) (f:=fun i =>(-1) ^ (k - i+1) * ↑(k.choose (i-1)) * f (x +↑i))]
      congr 1;ext i
      congr 1
      simp
      congr
      sorry
    conv_lhs=>enter [1];rw [range_eq_Ico,eq1]
    have eq2 : ∑ i ∈ range (k + 1), ↑(-1:ℤ ) ^ (k - i) * ↑(k.choose i) * f (x + ↑i) = ∑ i ∈ range (k + 1+1), ↑(-1) ^ (k - i) * ↑(k.choose i) * f (x + ↑i):= by
      symm
      rw [Finset.sum_range_succ]
      rw [Nat.choose_eq_zero_of_lt]
      simp
      linarith

    rw [eq2]
    sorry


structure ListOfSimilarPolyEval (f : ℤ → ℤ) (d : ℕ) (coeff: ℤ) where
  p : ℤ[X]
  h : p.natDegree = d
  hcoeff : p.leadingCoeff = coeff
  h_eq : ∀ i, f i = p.eval i

def diff_descend_degree {f : ℤ → ℤ} {d : ℕ} {coeff : ℤ}(lf : ListOfSimilarPolyEval f d coeff) :
    ListOfSimilarPolyEval (diff f) (d-1) (coeff * d) := by


  sorry

def diff_descend_degree_n_times {f : ℤ → ℤ} {n : ℕ} {coeff : ℤ}
    (lf : ListOfSimilarPolyEval f n coeff) :
    ListOfSimilarPolyEval (diff^[n] f) 0 (coeff * n.factorial) :=
  match n with
  | 0 => by
    simp
    exact lf
  | n+1 => by
    let aux := diff_descend_degree lf
    have : n+1 - 1 = n := by rfl
    simp_rw [this] at aux
    let auxaux := diff_descend_degree_n_times aux
    have : coeff * (n+1:ℕ) * n.factorial = coeff * (n+1).factorial := by
      rw [mul_assoc]; rfl
    rw [this] at auxaux
    have : diff^[n] (diff f) = diff^[n+1] f := rfl
    rw [this] at auxaux
    exact auxaux

def diff_descend_degree_n_times_on_zero_degree {f : ℤ → ℤ} {n : ℕ} {coeff : ℤ} (hn : n > 0)
    (lf : ListOfSimilarPolyEval f 0 coeff) :
    ListOfSimilarPolyEval (diff^[n] f) 0 0 := by
  let hlf := lf.h
  let hcoeff := lf.hcoeff
  have : ∀ i, f i = C coeff := fun i => by
    unfold leadingCoeff at hcoeff
    rw [hlf] at hcoeff
    rw [lf.h_eq i]
    rw [eq_C_of_natDegree_eq_zero hlf]
    rw [hcoeff]
    simp? says simp only [eq_intCast, eval_intCast, Int.cast_id]
  sorry

#check eq_C_of_natDegree_eq_zero

theorem diff_n_times_on_pow_k {n : ℕ} {k : ℕ} (h : k < n):
    (diff^[n]) (fun x => ((X: ℤ[X]) ^ k).eval x) = 0 := by
  sorry

theorem diff_n_times_on_pow_n (n : ℕ):
    (diff^[n]) (fun x => ((X: ℤ[X]) ^ n).eval x) = n.factorial := by
    sorry

when I try to def and prove difference Operatorand,I cannot compelete it,can help me compelete sorry?

[Kevin Buzzard]

Which sorry? There are many!

[SHAO YU]

After the second one, especially the second one :sweat_smile:

[SHAO YU]

I don't know how to define a new thing by myself yet. This is a framework written by capable people for me, but I don't have the ability to complete the code yet. It's not that I'm lazy and don't want to write code. Thank you