Re: [isabelle] Reindexing series



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
Description: This is a digitally signed message part



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