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