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
