Hi, I need to prove and then use a simple property of positive infinite summations, i.e. if the summation `f(0)+f(1)+...` converges, the limit of its "remainder after item n", i.e. `f(n)+f(n+1)+...` must be zero. Current HOL4 doesn't provide this lemma, I haven't looked into Isabelle yet (don’t know which file to look at …)
I know how to prove it by pencil and paper, but I don't know how to express
"remainder after item n" and its limit in a good way.
I'm dealing with extended reals, thus if that limit is `suminf_tail f`, my
desired lemma would be like this:
|- !f. (!n. 0 <= f n) /\ suminf f < PosInf ==> (suminf_tail f = 0)
So far I found two ways to define `f(n)+f(n+1)+...` given f and n. The first
way is to shift the argument by n:
(\n. suminf (\i. f (n + i))))
the second way is to forcely change the value of f(i) to zero if it's less than
n:
(\n. suminf (\i. if i < n then 0 else f i))
when n increasing above remainder as a function of n must decrease, thus to get
the limit ("-->" is not available in extrealTheory) I can use "inf" instead:
suminf_tail f = extreal_inf (IMAGE (\n. suminf (\i. f (n + i))) UNIV)
or
suminf_tail f = extreal_inf (IMAGE (\n. suminf (\i. if i < n then 0 else f
i)) UNIV)
In the first way, I worry about the (n + i) part, which may brings difficulties
apply arithmetic laws. In the second way, case analysis at such a deep nested
level also scares me.
Does anyone have similar experiences? Which one of the two definitions above
may be easier to handle? Are they correct? Is there any better way?
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
