# [isabelle] Reindexing series

Dear all,

`I want to prove that the order of summation of a converging sequence of non-negative reals
``does not matter. In Complex_Main, I'd express this as follows;
`
lemma
fixes f :: "nat => real"
assumes "summable f"
and "bij g"
and "!!x. 0 <= f x"
shows summable_reindex: "summable (f o g)"
and suminf_reindex: "suminf (f o g) = suminf f"

`My problem is that I have no clue how to prove this in Isabelle, because I am not so
``familiar with the details of limits in Isabelle. I expect that I could prove
``summable_reindex using the lemma summable_Cauchy, but the proof definitely will not be
``elegant. So I wonder:
`
1. Is a better way to prove summable_reindex?
2. How can I prove suminf_reindex?
3. Can I generalise the type real to some type class (which)?
Thanks in advance for any help,
Andreas

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