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


_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to