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



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