(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 > On Wed, Feb 12, 2020 at 8:31 PM Steve Rodriguez <[email protected]> wrote: > After the lcm proofs > <https://github.com/metamath/set.mm/commit/e856261581defcb02fe468b41eea1c6f56fb487f>, > 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 <http://us.metamath.org/mpeuni/df-zeta.html> 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 > <https://www.ams.org/journals/proc/1994-120-02/S0002-9939-1994-1172954-7/S0002-9939-1994-1172954-7.pdf>, > and says it > was "Conjectured by Knopp and first proved by Hasse > <http://www.home.earthlink.net/~jsondow/>", but Blagouchine > <http://math.colgate.edu/~integers/sjs3/sjs3.pdf> says > it was first proved by Mathias Lerch (for which a generalized zeta > function <https://en.wikipedia.org/wiki/Lerch_zeta_function> is > named) back in 1897. (I found the referenced proof online > <https://www.biodiversitylibrary.org/item/105783#page/49/mode/1up>.) > > 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™ > <http://metamath.tirix.org/df-zeta.html>. > > 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 > <https://youtu.be/Dzwm34w1UQI?t=194>: 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 > <https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem>; > currently > set.mm has binom <http://us.metamath.org/mpeuni/binom.html> for integers > and similar theorems for rising > <http://us.metamath.org/mpeuni/binomrisefac.html> and falling > <http://us.metamath.org/mpeuni/binomfallfac.html> > 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 > <http://us.metamath.org/mpeuni/cvgrat.html>, 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 > > -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/3c77ed15-40aa-4c1a-9758-c4282ba73816%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/3c77ed15-40aa-4c1a-9758-c4282ba73816%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStkFemsSEu6nerhuoX0ZxT-a7pzZdgNY9u8aHsFK1SWuQ%40mail.gmail.com.
