Re: [isabelle] Reindexing series



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



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