*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 19:43:24 +0100*In-reply-to*: <1416244904.998.2.camel@kit.edu>*References*: <5469C2C7.1040801@inf.ethz.ch> <1416244904.998.2.camel@kit.edu>

Hi, Am Montag, den 17.11.2014, 18:21 +0100 schrieb Joachim Breitner: > 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. yes, it’s possible without, and actually nicer: theory Scratch imports Complex_Main begin lemma fixes f :: "nat => real" assumes "summable f" and "inj g" and pos: "!!x. 0 <= f x" shows summable_reindex: "summable (f o g)" and suminf_reindex_aux: "suminf (f o g) ≤ suminf f" proof- have "∀ n. ∀ n' ∈ (g ` {..<n}). n' < Suc (Max (g ` {..<n}))" by (metis Max_ge finite_imageI finite_lessThan not_le not_less_eq) hence "∀ n. ∃ m. ∀ n'<n. g n' < m" by auto then obtain M :: "nat ⇒ nat" where n: "∀ n n'. n' < n ⟶ g n' < M n" by metis have inj: "⋀ S. inj_on g S" using `inj g` by (metis injD inj_onI) have smaller: "⋀n. (∑i<n. f (g i)) ≤ suminf f" proof- fix n have "setsum f (g ` {..<n}) ≤ (∑i<M n. f i)" by (rule setsum_mono3) (auto simp add: pos n[rule_format]) hence "(∑i<n. f (g i)) ≤ (∑i<M n. f i)" by (simp add: setsum.reindex[OF inj]) also have "… ≤ suminf f" using `summable f` by (rule setsum_le_suminf) (simp add: pos) finally show "(∑i<n. f (g i)) ≤ suminf f". qed have "incseq (λn. ∑i<n. f (g i))" by (rule incseq_SucI) (auto simp add: pos) moreover have "∀n. (∑i<n. f (g i)) ≤ suminf f" by (auto intro: smaller) ultimately obtain L where L: "(λ n. ∑i<n. f (g i)) ----> L" by (rule incseq_convergent) hence "(f ∘ g) sums L" by (simp add: sums_def) thus "summable (f o g)" by (auto simp add: sums_iff) from `(f ∘ g) sums L` have "suminf (f ∘ g) = L" by (auto simp add: sums_iff) from L have "L ≤ suminf f" by (rule LIMSEQ_le_const2) (auto intro: smaller) with `_ = L` show "suminf (f o g) ≤ suminf f" by simp qed lemma fixes f :: "nat => real" assumes "summable f" and "bij g" and pos: "!!x. 0 <= f x" shows suminf_reindex: "suminf (f o g) = suminf f" proof- from `bij g` have "inj g" by (rule bij_is_inj) from `bij g` have [simp]: "⋀ x. g (inv g x) = x" by (metis bij_betw_imp_surj surj_f_inv_f) show "suminf (f o g) = suminf f" proof (rule antisym) show "suminf (f ∘ g) ≤ suminf f" by (rule suminf_reindex_aux[OF `summable f` `inj g` pos]) next have "summable (f ∘ g)" by (rule summable_reindex[OF `summable f` `inj g` pos]) moreover from `bij g` have "inj (inv g)" by (metis bij_betw_def surj_imp_inj_inv) moreover from pos have "⋀ x. 0 ≤ (f ∘ g) x" by simp ultimately have "suminf ((f ∘ g) ∘ inv g) ≤ suminf (f ∘ g) " by (rule suminf_reindex_aux) thus "suminf f ≤ suminf (f ∘ g)" by (simp add:comp_def) qed qed And now I got to run, my colleages are going to watch a movie and I’m already late. Stupid addictivity of Isabelle :-) 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:*Andreas Lochbihler

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

**Re: [isabelle] Reindexing series***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Reindexing series
- Next by Date: [isabelle] Isabelle/PIDE as IDE for Standard ML
- 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