# Re: [isabelle] Reindexing series

```Hi,

Am Montag, den 17.11.2014, 10:41 +0100 schrieb Andreas Lochbihler:
> 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.

it’s not so bad, using the sandwich theorem I gave it a shot and did all
real-related proof-steps. There are just two holes related to "nat ⇒
nat" functions left as an exercise for the reader :-)

theory Scratch imports Complex_Main begin

lemma
fixes f :: "nat => real"
assumes "summable f"
and "bij g"
and pos: "!!x. 0 <= f x"
shows summable_reindex: "summable (f o g)"
and suminf_reindex: "suminf (f o g) = suminf f"
proof-
obtain m :: "nat ⇒ nat" where  "subseq m" and "∀ n n'. n' < m n ⟶ inv g n' < n" sorry
hence m: "⋀  n. {..<m n} ⊆ g ` {..<n}"
by (auto simp add: lessThan_def, metis (mono_tags) assms(2) bij_image_Collect_eq mem_Collect_eq)
obtain M :: "nat ⇒ nat" where "subseq M" and n: "∀ n n'. n' < n ⟶ g n' < M n" sorry

have inj: "⋀ S. inj_on g S" using  `bij g` by (metis bij_is_inj injD inj_onI)

have "(λn. ∑i<n. f (g i)) ----> suminf f"
proof (rule real_tendsto_sandwich[OF eventually_sequentiallyI  eventually_sequentiallyI])
fix n
have "(∑i<m n. f i) ≤ setsum f (g ` {..<n})"
by (rule setsum_mono3) (auto simp add: pos m)
thus "(∑i<m n. f i) ≤ (∑i<n. f (g i))"
next
fix n
have "setsum f (g ` {..<n}) ≤ (∑i<M n. f i)"
by (rule setsum_mono3) (auto simp add: pos n[rule_format])
thus "(∑i<n. f (g i)) ≤ (∑i<M n. f i)"
next
from `summable f`
have "(λx. setsum f {..<x}) ----> suminf f" by (metis summable_LIMSEQ)
from LIMSEQ_subseq_LIMSEQ[OF this `subseq m`]
show "(λx. setsum f {..<m x}) ----> suminf f"
next
from `summable f`
have "(λx. setsum f {..<x}) ----> suminf f" by (metis summable_LIMSEQ)
from LIMSEQ_subseq_LIMSEQ[OF this `subseq M`]
show "(λx. setsum f {..<M x}) ----> suminf f"
qed
hence "(f ∘ g) sums suminf f" by (simp add: sums_def)
thus "summable (f o g)" and  "suminf (f o g) = suminf f"
qed

The "subseq" requirement might be a bit too strong, but I did not see a
lemma like LIMSEQ_subseq_LIMSEQ (X ----> L ⟹ subseq f ⟹ (X ∘ f) ----> L)
that would allow repeating elements.

Hope it helps.

Greetings
Joachim

--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
```

Attachment: signature.asc
Description: This is a digitally signed message part

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