[isabelle] Reindexing series
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;
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and