Hello Mr. Saitoh, 1. I'm not professor, I'm first-year PhD. 2. your recent behaviors on Isabelle and HOL's mailing list have hurt the reputation of Japanese (or even Asian) researchers. 3. I'm not interested in your paper - actually I'm against any arithmetic with division-by-zero.
So please don't do this again. --Chun On Fri, Mar 1, 2019 at 10:12 PM Saburou Saitoh <saburou.sai...@gmail.com> wrote: > Dear Professors Tian and Zhang: > > I am very interesting your communication on summable, however, I would > like to read them carefully. > We got a new idea; the area of disc with radius r is of course \pi r^2, > however for r = infinity; in the entire plane, its area is zero!!. > > I will send some related article by separate e-mail. > > However, please look this: > > [5] *viXra:1902.0240 <http://vixra.org/abs/1902.0240>* *submitted on > 2019-02-13 22:57:25*, (0 unique-IP downloads) > > *Zero and Infinity; Their Interrelation by Means of Division by Zero* > > *Authors:* *Saburou Saitoh <http://vixra.org/author/saburou_saitoh>* > *Category:* General Mathematics <http://vixra.org/math> > > > > With best regards, > > Sincerely yours, > > > Saburou Saitoh > > 2019.3.2.6:11 > > > > > 2019年3月2日(土) 5:47 Chun Tian (binghe) <binghe.l...@gmail.com>: > >> there’s is a typo in my previous post. I wanted to ask “…, why f must >> *not* be summable?” (i.e. divergent) >> >> On a second thought, your approach could work for proving the partial sum >> is unbounded: for any real number e > 0, I can first use >> Archimedean property (simple version) of reals to find an integer N such >> that e < N, then I repeat N times your approach, first let the partial sum >> >= 1, then >= 2, … finally >= N, by induction, then the whole proof >> finished. However to implement this idea it’s not easy to me. Still want >> to know better proofs. >> >> —Chun >> >> > Il giorno 01 mar 2019, alle ore 20:54, Chun Tian (binghe) < >> binghe.l...@gmail.com> ha scritto: >> > >> > Hi Haitao, >> > >> > thanks, and yes, f is a sequence of reals. I'm following a similar path >> > (proof by contradiction), but I don't understand the last step: for any >> > m, the partial sum of f goes up by 1 at n > m, why f must be summable? I >> > think for every monotonic sequence such properties hold. >> > >> > --Chun >> > >> > Il 01/03/19 17:24, Haitao Zhang ha scritto: >> >> You say f is a function. From the context I assume the domain is Nat or >> >> f is a sequence. Mathematically speaking, you should form the partial >> >> sums of f ( sum f from 1 to n), which is a monotonic sequence of nats. >> >> Now proof by contradiction: if your conclusion doesn’t hold, for any m, >> >> you can find n > m, such that f n = 1. Then the partial sum goes up by >> 1 >> >> at n. As m is arbitrary, f is not summable. >> >> >> >> However I don’t know what is the best way to carry out the above proof >> >> in hol as I am not familiar with the relevant libraries yet. >> >> >> >> Haitao >> >> >> >> On Friday, March 1, 2019, Chun Tian (binghe) <binghe.l...@gmail.com >> >> <mailto:binghe.l...@gmail.com>> wrote: >> >> >> >> Hi, >> >> >> >> I'm blocked at the following goal: >> >> >> >> I have a function f returning either 0 or 1. Now I know the >> infinite >> >> sum of f is finite, i.e. >> >> >> >> suminf f < PosInf (or `summable f` speaking reals) >> >> >> >> How can I prove the set of {x | f x = 1} is finite, or after certain >> >> index m all the rest f(n) are zeros? >> >> >> >> ∃m. ∀n. m ≤ n ⇒ (f n = 0) >> >> >> >> If I use CCONTR_TAC (proof by contradiction), I can easily derive >> the >> >> following 2 assumptions using results I established in my previous >> >> similar questions: >> >> >> >> INFINITE N >> >> ∀n. n ∈ N ⇒ (f n = 1) >> >> >> >> but still I've no idea how to derive a contradiction with `suminf f >> < >> >> PosInf` by proving `suminf f = PosInf`... >> >> >> >> Thanks, >> >> >> >> Chun Tian >> >> >> > >> >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> > -- ---- Chun Tian (binghe) Fondazione Bruno Kessler (Italy)
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
