# 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)"
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

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.