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