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)
> <binghe.l...@gmail.com <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)
> <binghe.l...@gmail.com <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)
> <binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>
> >> <mailto: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
> >>
> >
>
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
