derivative commutes with infinite sum

Stream: Is there code for X?

[Eric Wieser]

Do we have any of these (likely under more assumptions than I wrote)?

import topology.algebra.infinite_sum
import analysis.calculus.deriv

variables {ι 𝕜 α β : Type*}
variables [nontrivially_normed_field 𝕜] [normed_add_comm_group α] [normed_add_comm_group β]
variables [normed_space 𝕜 α] [normed_space 𝕜 β]

lemma fderiv_tsum {f : ι → α → β} :
  fderiv 𝕜 (∑' i, f i) = ∑' i, fderiv 𝕜 (f i) := sorry

lemma has_deriv_at_tsum {f : ι → α → β} {f' : ι → α →L[𝕜] β}
  (x : α) (h : ∀ i, has_fderiv_at (f i) (f' i) x) :
  has_fderiv_at (∑' i, f i) (∑' i, f' i : α →L[𝕜] β) x := sorry

lemma has_deriv_at_of_has_sum {f : ι → α → β} {fs : α → β} {f' : ι → α →L[𝕜] β} {fs' : α →L[𝕜] β}
  (hfs : has_sum f fs) (hfs' : has_sum f' fs')
  (x : α) (h : ∀ i, has_fderiv_at (f i) (f' i) x) :
  has_fderiv_at fs fs' x := sorry

It feels like there's a rather large API to look for here, given tsum/has_sum/summable and deriv/fderiv/has_fderiv_at/has_deriv_at

[Sebastien Gouezel]

Yes. Look around docs#has_fderiv_at_tsum. You will need your field to be is_R_or_C, though, because otherwise you won't get any correct and useful version.

[Eric Wieser]

darn, I must just have not had that imported. Thanks!

[Kevin Buzzard]

is_R_or_Rbar should be enough

[Sebastien Gouezel]

Definitely, yes. You just need your field to contain R (and that's the way it's proved).

[Eric Rodriguez]

What goes wrong with other fields?

[Sebastien Gouezel]

You need some uniformity to control the tails. For this the key point is to use that if a function is differentiable on a ball with derivative bounded by C, then it is C-lipschitz there. This is wrong over general fields.

[Kevin Buzzard]

e.g. over the p-adics any locally constant continuous function is differentiable with derivative bounded by 0, but it may not be constant.