[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.