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.
On Wednesday, February 12, 2020 at 11:31:40 PM UTC-5, Steve Rodriguez 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/175e3459-8b70-4da0-8ef9-e9361826daaa%40googlegroups.com.
