Differentiability of a function defined using `list.foldr`

Stream: new members

[Quinn Culver]

How can differentiability of a function defined using list.foldr be proven?

My goal is to prove lemma test_fcn_differentiable in the MWE below.

import Mathlib

variable (x:ℝ )

def l := [1,2]

--the function x^2 + 2x^2
noncomputable def test_fcn : ℝ :=
  l.foldr (λ (n:ℕ ) (tf:ℝ)  => tf + n*x^2) 0

--the function 2x+4x
noncomputable def test_fcn_deriv : ℝ :=
  l.foldr (λ n (tfd:ℝ ) => tfd + 2*n*x ) 0

lemma test_fcn_differentiable: HasDerivAt
(fun x => test_fcn x) (test_fcn_deriv x) x  := by

  sorry

Secondary question: would it be better to use list.map and then list.sum instead of list.foldr?

[Richard Osborn]

My gut says you want a theorem like

variable [NontriviallyNormedField α] (f : β → α → α) (f' : β → α)

example (x : α) (h : ∀ n : β, HasDerivAt (f n) (f' n) x) (m : FreeAddMonoid β) :
    HasDerivAt (FreeAddMonoid.lift f m) (FreeAddMonoid.lift f' m) x := by sorry

I believe its true without any additional assumptions?

[Richard Osborn]

Hacked together a quick solution

import Mathlib

lemma foo [NontriviallyNormedField α] (f : β → α → α) (f' : β → α)
    (x : α) (h : ∀ n : β, HasDerivAt (f n) (f' n) x) (m : FreeAddMonoid β) :
    HasDerivAt (FreeAddMonoid.lift f m) (FreeAddMonoid.lift f' m) x := by
  induction m using FreeAddMonoid.recOn
  case h0 => simp [hasDerivAt_iff_tendsto]
  case ih n ns ih =>
    simp only [map_add, FreeAddMonoid.lift_eval_of, Pi.add_def, HasDerivAt.add (h n) ih]

variable (n : ℕ) (x : ℝ)

def m := FreeAddMonoid.ofList [1,2]

def f := n * x^2

def f' := 2 * n * x

--the function x^2 + 2x^2
noncomputable def test_fcn : ℝ → ℝ :=
  FreeAddMonoid.lift f m

--the function 2x + 4x
noncomputable def test_fcn_deriv : ℝ → ℝ :=
  FreeAddMonoid.lift f' m

lemma f_differentiable : HasDerivAt (f n) (f' n x) x := by
  unfold f; unfold f'
  rw [mul_comm 2, mul_assoc]
  suffices HasDerivAt (fun x => x ^ 2) (2 * x) x from HasDerivAt.const_mul (↑n) this
  convert hasDerivAt_pow 2 x
  simp

lemma test_fcn_differentiable : HasDerivAt test_fcn (test_fcn_deriv x) x := by
  unfold test_fcn; unfold test_fcn_deriv;
  exact foo f (f' · x) x (fun i => f_differentiable i x) m