*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Reindexing series*From*: Joachim Breitner <breitner at kit.edu>*Date*: Mon, 17 Nov 2014 18:21:44 +0100*In-reply-to*: <5469C2C7.1040801@inf.ethz.ch>*References*: <5469C2C7.1040801@inf.ethz.ch>

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))" by (simp add: setsum.reindex[OF inj]) 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)" by (simp add: setsum.reindex[OF inj]) 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" by (simp add: comp_def) 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" by (simp add: comp_def) qed hence "(f ∘ g) sums suminf f" by (simp add: sums_def) thus "summable (f o g)" and "suminf (f o g) = suminf f" by (auto simp add: sums_iff) 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**

**Follow-Ups**:**Re: [isabelle] Reindexing series***From:*Joachim Breitner

**References**:**[isabelle] Reindexing series***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Reindexing series
- Next by Date: Re: [isabelle] Reindexing series
- Previous by Thread: Re: [isabelle] Reindexing series
- Next by Thread: Re: [isabelle] Reindexing series
- Cl-isabelle-users November 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list