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.
