Ha! that’s smart … thanks! —Chun
> Il giorno 19 feb 2019, alle ore 17:23, buday.gerg...@uni-eszterhazy.hu ha > scritto: > > Chun, > > how about defining the sum of the tail as Limit minus the finite sum of the > first n elements? > > - Gergely > > Az Android Outlook <https://aka.ms/ghei36> letöltése > > > > > On Tue, Feb 19, 2019 at 5:10 PM +0100, "Chun Tian (binghe)" > <binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>> wrote: > > 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
