Riemann-zeta ratio-test rabbit-hole

[Steve Rodriguez]

After the lcm proofs, I decided to look at the "Zeta function" section in Mario
Carneiro's mathbox: df-zeta and zetacvg and the "hidden" cxpfd* and zeta*

theorems commented out after the two.  It was all...very educational for me.

(Long rambly notes on my experience follow.)

df-zeta appears to be what I'll call the Lerch-Knopp-Hasse-Sondow series form
of the Riemann zeta function: Jonathan Sondow proved it in 1994, and says it
was "Conjectured by Knopp and first proved by Hasse", but Blagouchine says
it was first proved by Mathias Lerch (for which a generalized zeta function is
named) back in 1897.  (I found the referenced proof online.)

The version in set.mm MIGHT be missing a "-u" for the final "^c s", but it is

complicated enough that I've surely misread, even in Structur-O-Vision™.

The hidden statements...oh boy, where to start?  The cxpfd* ones are evidently
to show that zeta converges to an actual number everywhere but s=1, but they've
proven to be like a hidden Final Fantasy video game boss: satisfying to find,

painful to attempt.  Around May of last year I'd tried to prove them for the

giggles, tipped off by the curious "~~? zetaalt" in df-zeta's comment, but

quickly switched elsewhere; after the lcm proofs, I tried again and got

cxpfdfval~cxpfditg figured out...sort of: cxpfd0 needed a

  $e |- S e. CC $.
hyp to be in any way provable, cxpfditg turned out to be false when N<K (after
struggling to prove as given, I found counterexamples for that case with SymPy
in a Jupyter notebook I set up), and though I was able to prove cxpfddif, I saw
the proof was basically a structural copy of binomlem.

That made me decide to try proving the general binomial theorem; currently
set.mm has binom for integers and similar theorems for rising and falling
factorials, but none of those are quite that.  I got to a crucial part (finding
the radius of convergence) and I found that cvgrat, our ratio test, seems to
work differently from the usual limit-based version: cvgrat.7 instead wants
proof that each step doesn't exceed than a real multiple of the one before, and
seems to require a specific value where the inequality starts to hold.

That's probably not impossible for me, but the proof would be much easier if I
could just say abs(C-x)/(x+1) ~~> 1 and thus the ratio test gives a radius of
cvg of 1.  For now I've dug further down the rabbit hole and started trying to
prove a cvgcmp2 to see if that can do away with the specific-value need:
    cvgcmp2.z $e |- Z = ( ZZ>= ` M ) $.
    cvgcmp2.f $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR ) $.
    cvgcmp2.g $e |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR ) $.
    cvgcmp2.cvg $e |- ( ph -> seq M ( + , F ) e. dom ~~> ) $.
    cvgcmp2.le $e |- ( ph -> E. n e. Z A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\
        ( G ` k ) <_ ( F ` k ) ) ) $.
    cvgcmp2 $p |- ( ph -> seq M ( + , G ) e. dom ~~> ) $=
      ? $.
...that is, replace hyps 2, 6, and 7 of cvgcmp with a single hyp that there
exists an n in Z that makes both inequalities true.  Then from there I could do
a new cvgcmpce and cvgrat.  It *seems* possible, if perhaps beyond me.

All in all, it's only convinced me more that mathematics is the greatest

magic.  And mathematicians its witches, and sugar and caffeine its potions...

Steve

[Mario Carneiro]

(resend for the benefit of the list)

It's nice to see that you're picking up where I left off in working on the zeta function. I'm still not even sure if that formula is the right approach; it is not well known and proofs about it were hard to find. The standard definition is as the analytic continuation of the usual sum converging for Re(s) > 1, but this begs the question of why the continuation exists, and so you need an explicit formula anyway.

zetaalt is a nice formula for evaluating the zeta function in a region that at least includes the mysterious critical strip. An alternate way to prove the existence of an analytic continuation is to combine this formula with the reflection formula, which relates zeta(s) to zeta(1-s), thus covering the plane with the overlapping regions Re(s) > 0 and Re(s) < 1.

I wish I still had my notes on the origin of this formula. I recall it being based on Euler summation of the standard series. If you use Cesaro summation on the zeta series, it converges for Re(s) > 0, and if you do it again it converges for Re(s) > -1; you can repeat the averaging n times to get it to converge above 1-n, and Euler summation is a way to do all of them in some coherent way so that it converges everywhere. But maybe you already know this since you have attached more names and proofs to this fact than I did. The formula is mentioned at https://en.wikipedia.org/wiki/Dirichlet_eta_function#Numerical_algorithms (where the Dirichlet eta function is apparently another name for the alternating zeta function), and it appears you are right about the missing negative sign at "^c s".

The cxpfd* theorems are completely untested, so I'm not surprised you are finding missing basic things like S e. CC. As you can tell it's more of a sketch than an actual proof, and I usually work out the exact assumptions as I go.

I forget why exactly I was interested in this sequence or proving that it goes to zero. (Wait, that statement is nonsense, F isn't a sequence. It looks like the definition of F was revised after the statements of cxpfdle and cxpfdcvg.) I think it is the proof of correctness of Euler summation applied in the specific case of the alternating zeta series. I am not sure if cxpfditg needs another domain but it seems plausible that we can assume N<K.

> and though I was able to prove cxpfddif, I saw proof was basically a structural copy of binomlem.

I suspect you've stumbled on some big generalization. While you are at it, you might want to see if it extends to Dirichlet L-functions and generalized zeta.

> I got to a crucial part (finding the radius of convergence) and I found that cvgrat, our ratio test, seems to work differently from the usual limit-based version: cvgrat.7 instead wants proof that each step doesn't exceed than a real multiple of the one before, and seems to require a specific value where the inequality starts to hold.

This is equivalent to the limit formulation. To see why, suppose we have your assumptions:

     cvgcmp2.z $e |- Z = ( ZZ>= ` M ) $.
     cvgcmp2.f $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR ) $.
     cvgcmp2.g $e |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR ) $.
     cvgcmp2.cvg $e |- ( ph -> seq M ( + , F ) e. dom ~~> ) $.
     cvgcmp2.le $e |- ( ph -> E. n e. Z A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) ) $.
     cvgcmp2 $p |- ( ph -> seq M ( + , G ) e. dom ~~> ) $=
       ? $.

We can introduce n and thus get it into this form (for a different choice of ph):

     cvgcmp2.z $e |- Z = ( ZZ>= ` M ) $.
     cvgcmp2.f $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR ) $.
     cvgcmp2.g $e |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR ) $.
     cvgcmp2.cvg $e |- ( ph -> seq M ( + , F ) e. dom ~~> ) $.

     cvgcmp2.le $e |- ( ph -> ( N e. Z /\ A. k e. ( ZZ>= ` N ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) ) ) $.

     cvgcmp2 $p |- ( ph -> seq M ( + , G ) e. dom ~~> ) $=
       ? $.

(We try to pre-introduce all existentials in hypotheses by convention unless there is a very good reason not to.) But now this is justcvgcmp with arguments chunked up a little differently.

Since this seems to be the critical step you are missing, let me briefly sketch the proof of cvgcmp2 from cvgcmp:

1: |- ( ph -> E. n e. Z A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) )

3a: |- Z = ( ZZ>= ` M )

3b: |- ( ZZ>= ` n ) = ( ZZ>= ` n )

3c: |- ( ( ( ( ph /\ n e. Z ) /\ A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) ) /\ i e. Z ) -> ( F ` i ) e. CC )

3d: |- ( ( ( ( ph /\ n e. Z ) /\ A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) ) /\ i e. Z ) -> ( G ` i ) e. CC )

3e: |- ( ( ( ph /\ n e. Z ) /\ A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) ) -> seq M ( + , F ) e. dom ~~> )

3f: |- ( ( ( ( ph /\ n e. Z ) /\ A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) ) /\ i e. ( ZZ>= ` n ) ) -> 0 <_ ( G ` i ) )

3g: |- ( ( ( ( ph /\ n e. Z ) /\ A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) ) /\ i e. ( ZZ>= ` n ) ) -> ( G ` i ) <_ ( F ` i ) )

3:cvgcmp |- ( ( ( ph /\ n e. Z ) /\ A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) ) -> seq M ( + , G ) e. dom ~~> )

2:3:rexlimdva |- ( ph -> ( E. n e. Z A. k e. ( ZZ>= ` n ) ( 0 <_ ( G ` k ) /\ ( G ` k ) <_ ( F ` k ) ) -> seq M ( + , G ) e. dom ~~> ) )

qed:1,2:mpd |- ( ph -> seq M ( + , G ) e. dom ~~> )

it should be easy to see how to prove steps 3a-g. The variable rename k |-> i is necessary to avoid a DV clash, or alternatively you can change k to i in the hypothesis (the bound variable in A. k e. ( ZZ>= ` n ) ...) so that you can reuse k in cvgcmp and just weaken to the assumptions.

I wish you luck in your zeta journey! I will be very happy if you make it as far as zetacl, that's the main theorem as far as I am concerned. There is a hell of a lot of wishful thinking after that: zeta2 is the Basel problem (which I guess isn't so bad since it's already in set.mm in different clothes), zeta3irr is a Apery's theorem, which has only recently been formalized for the first time in isabelle, and zetazcs implies the prime number theorem. At least I didn't actually put the Riemann hypothesis in as a "theorem"! zeta(-1) = -1/12 is another popular data point, if you make it that far. The reflection theorem is the main workhorse for stuff about the negative values of zeta.

Mario

 

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3c77ed15-40aa-4c1a-9758-c4282ba73816%40googlegroups.com.

[Steve Rodriguez]

Yes, eta and Euler summation; Sondow cites Knopp's section on the latter.  And yes, F as such wouldn't work so I had prepared to try e.g. ( F ` K ) ~~> 0 for cxpfdcvg.

Indeed the rexlimdva trick (which reminds me of the old dedth pattern, and is slightly shortened with r19.29a) works quite easily to "retrofit" either of the cvgcmps with "E." hyps.  I'll see what I can pull off with that.

Thank you,

Steve

To unsubscribe from this group and stop receiving emails from it, send an email to meta...@googlegroups.com.

[Thomas Brendan Leahy]

I have to wonder, rather than using the iota trick there now, whether it might make more sense to use a limit of a quotient?  Only it seems like it'd be a lot less work to prove uniqueness and continuity that way.

[Steve Rodriguez]

Hello Brendan Leahy,

I'm not quite sure myself so I guess I'll burn that bridge when I get to it; I do know that I dread when I'll need to ultimately show that the series is not just *a* continuation of zeta but *the* single such, presumably with the currently unused df-ana or some equivalent system.  It'll be fun, for sure.

―

Speaking of dread, progress has been slow but I managed to prove

    cvgrat2.z $e |- Z = ( ZZ>= ` M ) $.
    cvgrat2.m $e |- ( ph -> M e. ZZ ) $.
    cvgrat2.f $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) $.
    cvgrat2.n0 $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) =/= 0 ) $.
    cvgrat2.r $e |- R = ( k e. Z |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) $.
    cvgrat2.cvg $e |- ( ph -> R ~~> L ) $.

    cvgrat2 $p |- ( ( ph /\ L < 1 ) -> seq M ( + , F ) e. dom ~~> ) $= ? $.

by using the r19.29a trick on cvgrat itself.  That took more steps than I'd've liked (120 when webpage'd), but didn't need the cvgcmp theorems and suggests that proving it as a separate statement from binomial-series lemmas was wise.  It also took longer than it should've, partly because at one point I was trying to derive

    ( abs ` ( F ` ( k + 1 ) ) ) <_ ( L x. ( abs ` ( F ` k ) ) )

instead of

    ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ),

where r e. ( L (,) 1 ), from R.  Just one letter can destroy a proof!

I still want to perhaps remove the n0 hyp; I *think* it's only necessary to have nonzero F(k) at k>N, not the full k>M, and I could probably imply that within the proof, probably not from hyp cvgrat.7 itself but maybe in tandem with cvgrat2.r.  That all doesn't seem strictly necessary for the binomial series, though, and I think it even more important to extend the result to

    cvgrat2 $p |- ( ph -> ( ( L < 1 -> seq M ( + , F ) e. dom ~~> ) /\ ( 1 < L -> seq M ( + , F ) e/ dom ~~> ) ) ) $= ? $.,

partly because (a) I can then more easily derive the exact value of R for pserdv2 (spoiler alert: 1) to continue with the proof and (b) I love the mirror duality of it!  L<1 and 1<L and all that.  (The whole beauty thing is also why I don't want to use "-. _ e. _" for the statement instead, even though e/ complicates proofs a bit...)

Edit: Or, since the hyps imply L e. RR, I can maybe just do

    cvgrat2 $p |- ( ( ph /\ L =/= 1 ) -> ( L < 1 <-> seq M ( + , F ) e. dom ~~> ) ) $= ? $.,

which would dodge the issue and shorten the statement.

Thank you,

Steve

[Mario Carneiro]

Once you prove that the sum converges everywhere on a dense set (namely the whole plane except 1 + 2 n pi i or something like that), uniqueness off the poles is trivial because real/complex sums are unique. Uniqueness at the poles is guaranteed by continuous extension in a hausdorff space.

You would need a much more high powered (but generic) theorem if the claim was that a unique analytic function extends the conventional sum that is defined for Re s > 1, because that's obviously not dense in the plane so you need to know some things about complex analysis for the proof.

On Fri, Feb 21, 2020 at 1:22 AM Steve Rodriguez <steve....@gmail.com> wrote:

Hello Brendan Leahy,

I'm not quite sure myself so I guess I'll burn that bridge when I get to it; I do know that I dread when I'll need to ultimately show that the series is not just *a* continuation of zeta but *the* single such, presumably with the currently unused df-ana or some equivalent system.  It'll be fun, for sure.

―

Speaking of dread, progress has been slow but I managed to prove

    cvgrat2.z $e |- Z = ( ZZ>= ` M ) $.
    cvgrat2.m $e |- ( ph -> M e. ZZ ) $.
    cvgrat2.f $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) $.
    cvgrat2.n0 $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) =/= 0 ) $.
    cvgrat2.r $e |- R = ( k e. Z |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) $.
    cvgrat2.cvg $e |- ( ph -> R ~~> L ) $.

    cvgrat2 $p |- ( ( ph /\ L < 1 ) -> seq M ( + , F ) e. dom ~~> ) $= ? $.

by using the r19.29a trick on cvgrat itself.  That took more steps than I'd've liked (120 when webpage'd), but didn't need the cvgcmp theorems and suggests that proving it as a separate statement from binomial-series lemmas was wise.  It also took longer than it should've, partly because at one point I was trying to derive

    ( abs ` ( F ` ( k + 1 ) ) ) <_ ( L x. ( abs ` ( F ` k ) ) )

instead of

    ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ),

where r e. ( L (,) 1 ), from R.  Just one letter can destroy a proof!

I still want to perhaps remove the n0 hyp; I *think* it's only necessary to have nonzero F(k) at k>N, not the full k>M, and I could probably imply that within the proof, probably not from hyp cvgrat.7 itself but maybe in tandem with cvgrat2.r.  That all doesn't seem strictly necessary for the binomial series, though, and I think it even more important to extend the result to

    cvgrat2 $p |- ( ph -> ( ( L < 1 -> seq M ( + , F ) e. dom ~~> ) /\ ( 1 < L -> seq M ( + , F ) e/ dom ~~> ) ) ) $= ? $.,

partly because (a) I can then more easily derive the exact value of R for pserdv2 (spoiler alert: 1) to continue with the proof and (b) I love the mirror duality of it!  L<1 and 1<L and all that.  (The whole beauty thing is also why I don't want to use "-. _ e. _" for the statement instead, even though e/ complicates proofs a bit...)

Thank you,

--

You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c9c6e8a2-18f0-4243-b48a-98531d10ad45%40googlegroups.com.

[Steve Rodriguez]

That makes sense, Mario, that I wouldn't need the heavy machinery to just fill in a few value holes instead of a whole half-plane.  Sondow says as such but I wasn't quiiiiite sure why when I first read it.

I've since replaced cvgrat2 with a finished proof of the combination of cvgrat and the divergence side,

    cvgdvgrat.z $e |- Z = ( ZZ>= ` M ) $.

    cvgdvgrat.w $e |- W = ( ZZ>= ` N ) $.
    cvgdvgrat.n $e |- ( ph -> N e. Z ) $.
    cvgdvgrat.f $e |- ( ph -> F e. V ) $.
    cvgdvgrat.c $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) $.
    cvgdvgrat.n0 $e |- ( ( ph /\ k e. W ) -> ( F ` k ) =/= 0 ) $.
    cvgdvgrat.r $e |- R = ( k e. W |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) $.
    cvgdvgrat.cvg $e |- ( ph -> R ~~> L ) $.
    cvgdvgrat.n1 $e |- ( ph -> L =/= 1 ) $.

    cvgdvgrat $p |- ( ph -> ( L < 1 <-> seq M ( + , F ) e. dom ~~> ) ) $= ? $.

and I'll probably submit that shortly.  I (think I) needed .f to contrapose serf0 (i.e. if F doesn't converge to zero then seqM(+,F) won't converge at all) for the divergence part.

From there I guess I can use that ratio test to derive Wikipedia's or ProofWiki's radius of cvg proof (seeing that the latter was separate from its proof of the ratio test made me realize that using the ratio test to test convergence and using that test's ratio to find the ROC seem subtly different things), and use pserdv2 for differential witchery to finish proving the binomial series, then try the cxpfd*s again (phew).

abelth may be relevant, but its main purpose seems to be for the value *at* the ROC circle.  I'll stay on the ratio path.

―

Edit 2020-03-07: Welp, that didn't get me too far.  The next step for me is radcnvrat,

    $( pser.g $)
    radcnvrat.g $e |- G = ( x e. CC |-> ( n e. NN0 |->
        ( ( A ` n ) x. ( x ^ n ) ) ) ) $.
    $( radcnv.a $)
    radcnvrat.a $e |- ( ph -> A : NN0 --> CC ) $.
    $( radcnv.r $)
    radcnvrat.r $e |- R =
        sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) $.
    radcnvrat.rat $e |- D = ( k e. NN0 |->
        ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) ) $.
    radcnvrat.z $e |- Z = ( ZZ>= ` M ) $.
    radcnvrat.m $e |- ( ph -> M e. NN0 ) $.
    radcnvrat.n0 $e |- ( ( ph /\ k e. Z ) -> ( A ` k ) =/= 0 ) $.
    radcnvrat.l $e |- ( ph -> D ~~> L ) $.
    radcnvrat.ln0 $e |- ( ph -> L =/= 0 ) $.

    radcnvrat $p |- ( ph -> R = ( 1 / L ) ) $= ? $.

With cvgdvgrat I can get

    |- ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) ->

         ( ( ( abs ` x ) x. L ) < 1 <-> seq 0 ( + , ( G ` x ) ) e. dom ~~> ) )

The antecedent becomes (...x e. CC...) if I add the zero case with radcnv0, and with radcnvrat.ln0 it becomes

    |- ( ( ( ph /\ x e. CC ) /\ ( abs ` x ) =/= ( 1 / L ) ) ->

         ( ( abs ` x ) < ( 1 / L ) <-> seq 0 ( + , ( G ` x ) ) e. dom ~~> ) )

or

    |- ( ( ph /\ x e. CC ) ->

         ( ( ( abs ` x ) < ( 1 / L ) -> seq 0 ( + , ( G ` x ) ) e. dom ~~> ) /\

           ( seq 0 ( + , ( G ` x ) ) e. dom ~~> -> -. ( 1 / L ) < ( abs ` x ) ) ) )

To me that's exactly what Wikipedia's ROC proof sketch is going for, but to be sure of that (and make it usable with pserdv2) I think I need to match it up with a supremum theorem like eqsup, eqsupd, supxr, or supxr2 that allows for the sup not necessarily being a member of { r e. RR | ... }.  It's obvious to me that 1/L is the sup—1/L is not necessarily a member of the convergence region, but no member is greater in absolute value than 1/L and any y even infinitesimally smaller than 1/L has members of the region sandwiched between y and 1/L—but I can't quite make the mental and mechanical (metamathechanical?) connection, even though it *feels* like it'd be just another case of Mario's proof sketch in the first reply or suchlike.  (Changing "( G ` x )" to "( G ` ( abs ` x ) )" by way of the idempotence of abs doesn't quite get me closer, but would help in changing all the "( abs ` x )"es to "y"...)

―

Edit 2020-03-08: Found another path to get radcnvrat done.  Verifying now and submitting soon.

―

Edit 2020-03-15: Still going.  I split the binomial-series proof in two.  The case for nonnegative-integer exponents is done; it needed a cvgcmpce to show convergence of the series so that I could isumsplit the sum over NN0 into the finite sum of binom and the zeroes after that, but it was easy besides.  I'll hold off on submitting until I've proven (more of) the non-nonnegative-integer case; I am just past getting the derivative of the series in the proof and splitting off that "e. NN0" case made verifying the ratio in the ROC part easier.  It'll require SF's mathboxed FallFac and prod_, and I'm mulling whether to also use oFC (and whether to redo expgrowth, done ~2 years before that arrived, with that...) or plain oF, for multiplying functions and such.

On Friday, February 21, 2020 at 12:28:05 PM UTC-5, Mario Carneiro wrote:

Once you prove that the sum converges everywhere on a dense set (namely the whole plane except 1 + 2 n pi i or something like that), uniqueness off the poles is trivial because real/complex sums are unique. Uniqueness at the poles is guaranteed by continuous extension in a hausdorff space.

You would need a much more high powered (but generic) theorem if the claim was that a unique analytic function extends the conventional sum that is defined for Re s > 1, because that's obviously not dense in the plane so you need to know some things about complex analysis for the proof.

To unsubscribe from this group and stop receiving emails from it, send an email to meta...@googlegroups.com.