The iterated derivative of a sum is the sum of the iterated

Stream: Is there code for X?

[Mark Andrew Gerads]

I am trying to take the iterated derivative of a sum, and thus need something like this:

theorem iteratedDerivSum {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1}
  {u : Finset ι} {A : ι → 𝕜 → F} (k : ℕ) (h : ∀ i ∈ u, ContDiff 𝕜 k (A i)) :
  iteratedDeriv k (fun y => Finset.sum u fun i => A i y) x = Finset.sum u fun i => iteratedDeriv k (A i) x := by
  sorry

I only need it for complex numbers but figure there should be a general version in mathlib.

[Mark Andrew Gerads]

I just built a similar theorem:

theorem iteratedDerivSum {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_1}
  {u : Finset ι} {A : ι → 𝕜 → F} (h : ∀ i ∈ u, ContDiff 𝕜 ⊤ (A i)) :
  ∀ (k : ℕ), iteratedDeriv k (fun y => Finset.sum u fun i => A i y) = (fun y => Finset.sum u fun i => iteratedDeriv k (A i) y) := by
  intros k
  induction' k with K Kih
  · simp only [iteratedDeriv_zero, Finset.sum_apply]
  · have h₀ := congrArg deriv Kih
    rw [iteratedDeriv_succ, h₀]
    clear h₀
    ext x
    have h₁ : (1 : ℕ∞) ≤ ⊤ := by exact OrderTop.le_top 1
    have h₂ : ∀ i ∈ u, DifferentiableAt 𝕜 (iteratedDeriv K (A i)) x := by
      intros i ih
      have h₃ := ContDiff.iterate_deriv K (h i ih)
      rw [←iteratedDeriv_eq_iterate] at h₃
      exact ContDiffAt.differentiableAt (ContDiff.contDiffAt h₃) h₁
    rw [deriv_sum h₂]
    simp_rw [iteratedDeriv_succ]

[Eric Wieser]

is this docs#map_finset_sum ?

[Eric Wieser]

Hmm, maybe the lemma I'm thinking of is in an open PR, let me find it

[Eric Wieser]

docs#MultilinearMap.map_sum_finset, which seems misnamed

[Eric Wieser]

I think this is the start of the right approach:

import Mathlib

variable
    {𝕜 : Type u} [NontriviallyNormedField 𝕜]
    {F : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]

@[simp]
theorem HasFTaylorSeriesUpTo.zero {k} :
    HasFTaylorSeriesUpTo (𝕜 := 𝕜) k (0 : E → F) 0 where
  zero_eq x := rfl
  fderiv _ _ x := hasFDerivAt_zero_of_eventually_const 0 (by simp)
  cont _ _ := continuous_const

theorem HasFTaylorSeriesUpTo.add
    {A B : E → F}
    {A' B' : E → FormalMultilinearSeries 𝕜 E F}
    (hA : HasFTaylorSeriesUpTo k A A')
    (hB : HasFTaylorSeriesUpTo k B B') :
    HasFTaylorSeriesUpTo k (A + B) (A' + B') where
  zero_eq x := congr($(hA.zero_eq x) + $(hB.zero_eq x))
  fderiv m hm x := (hA.fderiv m hm x).add (hB.fderiv m hm x)
  cont m hm := (hA.cont m hm).add (hB.cont m hm)

theorem HasFTaylorSeriesUpTo.sum
    {ι : Type u_1}
    {u : Finset ι} {A : ι → E → F}
    (A' : ι → E → FormalMultilinearSeries 𝕜 E F)
    (h : ∀ i, HasFTaylorSeriesUpTo (𝕜 := 𝕜) k (A i) (A' i)) :
    HasFTaylorSeriesUpTo k (fun y => Finset.sum u fun i => A i y) (fun y => Finset.sum u fun i => A' i y) := by
  induction u using Finset.cons_induction with
  | empty => exact .zero
  | cons a s ha ih =>
    simp_rw [Finset.sum_cons]
    exact .add (h _) ih

[Eric Wieser]

Or docs#iteratedFDeriv_sum