*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Reindexing series*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Mon, 17 Nov 2014 18:02:48 +0100*In-reply-to*: <5469C2C7.1040801@inf.ethz.ch>*Organization*: TU München*References*: <5469C2C7.1040801@inf.ethz.ch>

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. So I wonder: > > 1. Is a better way to prove summable_reindex? summable_reindex depends on the order of reals, it does not work without. So summable_Cauchy which is about metric is not so well suited. A better idea may be to use summation on extended reals, here you have suminf f = (SUP n. setsum f {..n}) and then antisymmetry (or better SUP_eq) to prove: (SUP n. setsum f {..n}) = (SUP n. setsum (f o g) {..n}) A attached a proof using HOL-Probability, as it uses the non-negative integral on ereals, which is very easy to proof. (especially with distr_bij_count_space which I will add to the repository...) > 2. How can I prove suminf_reindex? Prove it first on ereal and then reduce it to the reals (see my proof) > 3. Can I generalise the type real to some type class (which)? You need order, so maybe: {ordered_comm_monoid_add, linorder_topology, conditionally_complete_linorder} at least that's what I used for summableI_nonneg_bounded. real_normed_vectors do not work, as you need to state that you somehow always run in the same direction. - Johannes

theory Scratch imports Probability begin lemma distr_bij_count_space: assumes f: "bij_betw f A B" shows "distr (count_space A) (count_space B) f = count_space B" proof (rule measure_eqI) have f': "f \<in> measurable (count_space A) (count_space B)" using f unfolding Pi_def bij_betw_def by auto fix X assume "X \<in> sets (distr (count_space A) (count_space B) f)" then have X: "X \<in> sets (count_space B)" by auto moreover then have "f -` X \<inter> A = the_inv_into A f ` X" using f by (auto simp: bij_betw_def subset_image_iff image_iff the_inv_into_f_f intro: the_inv_into_f_f[symmetric]) moreover have "inj_on (the_inv_into A f) B" using X f by (auto simp: bij_betw_def inj_on_the_inv_into) with X have "inj_on (the_inv_into A f) X" by (auto intro: subset_inj_on) ultimately show "emeasure (distr (count_space A) (count_space B) f) X = emeasure (count_space B) X" using f unfolding emeasure_distr[OF f' X] by (subst (1 2) emeasure_count_space) (auto simp: card_image dest: finite_imageD) qed simp lemma nn_integral_bij_count_space: assumes g: "bij_betw g A B" shows "(\<integral>\<^sup>+x. f (g x) \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)" using g[THEN bij_betw_imp_funcset] by (subst distr_bij_count_space[OF g, symmetric]) (auto intro!: nn_integral_distr[symmetric]) lemma ereal_suminf_bij: fixes f :: "nat \<Rightarrow> ereal" assumes g: "bij g" shows "(\<And>n. 0 \<le> f n) \<Longrightarrow> (\<Sum>x. f (g x)) = (\<Sum>x. f x)" apply (subst (1 2) nn_integral_count_space_nat[symmetric]) apply (auto simp: g nn_integral_bij_count_space) done lemma summable_ereal_iff: "(\<And>i. 0 \<le> f i) \<Longrightarrow> summable f \<longleftrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>" by (metis suminf_ereal_finite summable_ereal) lemma summable_bij: fixes f :: "nat \<Rightarrow> real" assumes g: "bij g" shows "(\<And>x. 0 \<le> f x) \<Longrightarrow> summable (\<lambda>x. f (g x)) \<longleftrightarrow> summable f" by (simp add: summable_ereal_iff ereal_suminf_bij[OF g, of f]) lemma sums_bij: fixes f :: "nat \<Rightarrow> real" shows "bij g \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow> summable f \<Longrightarrow> (\<Sum>x. f (g x)) = suminf f" unfolding ereal.inject[symmetric] by (subst (1 2) suminf_ereal'[symmetric]) (auto simp: summable_bij intro!: ereal_suminf_bij) end

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

- Previous by Date: Re: [isabelle] Problem copying logical relation from TAPL
- Next by Date: Re: [isabelle] Reindexing series
- Previous by Thread: [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