Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Decomposing an Infinite Sum

view this post on Zulip Email Gateway (Aug 22 2022 at 19:17):

From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
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

Last updated: Nov 21 2024 at 12:39 UTC