# Re: [Hol-info] An infinite sum of 0 or 1 is finite, then ...

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.
>
>
> [5] *viXra:1902.0240 <http://vixra.org/abs/1902.0240>* *submitted on
>
> *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