[isabelle] Decomposing an Infinite Sum



Dear Isabelle/HOL experts and users,
  I am trying to prove a lemma about an infinite sum of zeros, but I can
only prove it assuming that some set is finite. Is there a way to prove it
without this restriction?

Concretely,

I proved lemma qValSumAunrestricted,
but I want to prove lemma qValSumAunrestrictedGeneral
in the following file:
https://github.com/josephcmac/miscellany/blob/master/qRHLvariables.thy

Kind Regards,
José Manuel Rodriguez Caballero



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.