f = g implies deriv f = deriv g

Stream: maths

[Mark Andrew Gerads]

I've been trying for a while and did not figure it out. Please help find the next step in ruesDiffIteratedDeriv, applying deriv to both sides of the equation K_ih.
image.png

import analysis.complex.basic
import analysis.calculus.deriv
import analysis.calculus.iterated_deriv

def ruesDiff (n : ℕ) (m : ℤ) : ℂ → ℂ := sorry

lemma ruesDiffHasDeriv (n : ℕ) (m : ℤ) (z : ℂ) :
  has_deriv_at (ruesDiff n m) (ruesDiff n (m + 1) z) z :=
begin
  sorry, -- already proved elsewhere
end

lemma ruesDiffDeriv (n : ℕ) (m : ℤ) :
  deriv (ruesDiff n m) = (ruesDiff n (m + 1)) :=
begin
  refine deriv_eq _,
  intros z,
  exact ruesDiffHasDeriv n m z,
end

lemma ruesDiffIteratedDeriv (k n : ℕ) (m : ℤ) (z : ℂ) : iterated_deriv k (ruesDiff n m) = ruesDiff n (k+m) :=
begin
  induction k with K K_ih,
  simp only [iterated_deriv_zero, nat.cast_zero, zero_add],
  -- -- the following 4 attemps all failed.

  -- {
  --   have h0 : deriv (iterated_deriv K (ruesDiff n m)) = deriv (ruesDiff n ((K:ℤ) + m)),
  --   exact congr_arg deriv,
  -- },

  -- simp_rw congr_arg deriv at K_ih,

  -- simp_rw congr_arg (deriv:(ℂ → ℂ) → (ℂ → ℂ)) at K_ih,

  -- simp_rw (congr_arg (λ (f : (ℂ → ℂ)), deriv f)) at K_ih,
  sorry,
end

[Andrew Yang]

Without actual looking in an IDE, I would guess congr_arg deriv K_ih works.

[Ruben Van de Velde]

You won't get anywhere without explicitly invoking ruesDiffDeriv

[Damiano Testa]

These two lines close the goal

  rw [iterated_deriv_succ, K_ih],
  exact (ruesDiffDeriv _ _),

[Ruben Van de Velde]

Stay with rw [iterated_deriv_succ, K_ih],, I think

[Ruben Van de Velde]

Ha, not as fast as Damiano