# Re: [isabelle] Reindexing series

```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:
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

```

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