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 <[email protected]> wrote: > Hello Brendan Leahy, > > I'm not quite sure myself so I guess I'll burn that bridge when I get to > it > <https://malaphors.com/2013/01/17/well-burn-that-bridge-when-we-come-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 <http://us.metamath.org/mpeuni/df-ana.html> > or some equivalent system. It'll be fun > <https://en.wikipedia.org/wiki/Dwarf_Fortress>, 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 <http://us.metamath.org/mpeuni/pserdv2.html> (spoiler alert: 1) > to continue with the proof > <https://en.wikibooks.org/wiki/Advanced_Calculus/Newton%27s_general_binomial_theorem> > 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, > Steve > > On Wednesday, February 19, 2020 at 11:54:47 PM UTC-5, Thomas Brendan Leahy > wrote: >> >> 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/c9c6e8a2-18f0-4243-b48a-98531d10ad45%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/c9c6e8a2-18f0-4243-b48a-98531d10ad45%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/CAFXXJStcmihkWoHTZebEoL2A%2Bzf%2Bw12YbtnnJU0zwisXBhxwaQ%40mail.gmail.com.
