function equal to id of function (norm iterated_fderiv)

Stream: Is there code for X?

[rtertr (Sonia)]

Good evening everyone,

Is there a theorem for proving that these two norms are equal?
Or would is it not logically true, and they have to be written in a different way?

import tactic
import analysis.special_functions.exp_deriv
import analysis.calculus.iterated_deriv

noncomputable theory

namespace real

lemma inner_product_to_one_dimensional1 {i:ℕ} {a:ℂ} {x:ℝ  }: ‖iterated_fderiv ℝ i (λ (x : ℝ ), x) (‖x‖) ‖ = ‖iterated_fderiv ℝ i (λ (x : ℝ ), ‖x‖) x ‖:=
begin
  simp only [real.norm_eq_abs],
  congr',
end

[Filippo A. E. Nuccio]

Well, what you are trying to prove is not true. For instance, in the special case i=1 after two rewrites one obtains

lemma inner_product_to_one_dimensional1 {a:ℂ} {x:ℝ }:
‖iterated_fderiv ℝ 1 (λ (x : ℝ ), x) (‖x‖) ‖ = ‖iterated_fderiv ℝ 1 (λ (x : ℝ ), ‖x‖) x ‖:=
begin
  rw norm_iterated_fderiv_eq_norm_iterated_deriv,
  rw iterated_deriv_one,
  rw norm_iterated_fderiv_eq_norm_iterated_deriv,
  rw iterated_deriv_one,
  simp,
end

with the goal ⊢ 1 = |deriv abs x| . Since the absolute value is not differentiable at 0, its derivative is defined to be 0 there, so the goal is actually ⊢ 1 = 0.