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

[Chun Tian (binghe)]

Thanks, my problem has been resolved using inductions.

I'm actually using extrealTheory. All I have for the necessary and
sufficient condition of a suminf being PosInf is the following:

   [ext_suminf_eq_infty]  Theorem

  ⊢ ∀f.
(∀n. 0 ≤ f n) ∧ (∀e. e < PosInf ⇒ ∃n. e ≤ ∑ f (count n)) ⇒
(suminf f = PosInf)

   [ext_suminf_eq_infty_imp]  Theorem

  ⊢ ∀f.
(∀n. 0 ≤ f n) ∧ (suminf f = PosInf) ⇒
∀e. e < PosInf ⇒ ∃n. e ≤ ∑ f (count n)

In my case, given any `e < PosInf`, it's very hard to construct such a
`n` directly, but, as I found before (based on your approach), an
induction approach works, and it turns out that the proof is quite
straightforward although not very short.

--Chun

Il 02/03/19 03:05, Haitao Zhang ha scritto:
> I assume you are using the theory from src/real/seqScript.sml and it
> looks like that summable is defined as a convergence of partial sums.
> That means you should be able to directly contradict the convergence
> criterion if (f n) does not go to 0. For example, SER_CAUCHY gives you:
> 
> “!f. summable f =
>   !e. &0 < e ==> ?N. !m n. m >= N ==> abs(sum(m,n) f) < e”
> 
> Choose e < 1, for any N, find n>N such that f n = 1, then abs(sum(n,n+1)
> f)=1 > e and contradiction. (I don't know the indexing of sum so it
> could be sum(n,n)).
> 
> Hope this helps,
> Haitao
> 
> 
> 
> On Fri, Mar 1, 2019 at 12:46 PM Chun Tian (binghe)
> mailto:binghe.l...@gmail.com>> wrote:
> 
> 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)
> mailto: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)
> 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
> >>
> >
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Haitao Zhang]

I assume you are using the theory from src/real/seqScript.sml and it looks
like that summable is defined as a convergence of partial sums. That means
you should be able to directly contradict the convergence criterion if (f
n) does not go to 0. For example, SER_CAUCHY gives you:

“!f. summable f =
  !e. &0 < e ==> ?N. !m n. m >= N ==> abs(sum(m,n) f) < e”

Choose e < 1, for any N, find n>N such that f n = 1, then abs(sum(n,n+1)
f)=1 > e and contradiction. (I don't know the indexing of sum so it could
be sum(n,n)).

Hope this helps,
Haitao



On Fri, Mar 1, 2019 at 12:46 PM Chun Tian (binghe) 
wrote:

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

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

[Chun Tian (binghe)]

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 
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 * *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 *
> *Category:* General Mathematics 
>
>
>
> With best regards,
>
> Sincerely yours,
>
>
> Saburou Saitoh
>
> 2019.3.2.6:11
>
>
>
>
> 2019年3月2日(土) 5:47 Chun Tian (binghe) :
>
>> 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) > >> > 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

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

[Saburou Saitoh]

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 * *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 *
*Category:* General Mathematics 



With best regards,

Sincerely yours,


Saburou Saitoh

2019.3.2.6:11




2019年3月2日(土) 5:47 Chun Tian (binghe) :

> 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)  >> > 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
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Chun Tian (binghe)]

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



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

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

[Chun Tian (binghe)]

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



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Haitao Zhang]

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