[Hol-info] Derivative of real infinite summation in HOL Light

[Elif D. <e_...@en...>]

Dear all,

I am working with infinite summation and real derivatives in HOL Light. I
can write a theorem for the derivative of the finite summation as follows:

g `!f s. FINITE s /\ (!a. a IN s ==> (f a has_real_derivative f' a)
(atreal t))
     ==> real_derivative  (\x. sum s (\a. f a x)) t = sum s f'`

and it is proved easily as well.

Now, I want to prove a similar theorem for the real derivative of the
infinite summation. However, I am unable to do that. I have tried a couple
of ways using the HOL Light function real_infsum but I have got no success
yet.

Could anybody guide me towards this theorem?

Best regards,
Elif Deniz