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
<https://en.wikipedia.org/wiki/Radius_of_convergence#Theoretical_radius> or
ProofWiki's
<https://proofwiki.org/wiki/Radius_of_Convergence_from_Limit_of_Sequence/Complex_Case>
radius of cvg proof (seeing that the latter was separate from its proof of
the ratio test <https://proofwiki.org/wiki/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
<http://us.metamath.org/mpeuni/pserdv2.html> for differential witchery to
finish proving the binomial series, then try the cxpfd*s again (phew).
abelth <http://us.metamath.org/mpeuni/abelth.html> may be relevant, but its
main purpose seems to be for the value *at* the ROC circle. I'll stay on
the ratio path.
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.
>
> On Fri, Feb 21, 2020 at 1:22 AM Steve Rodriguez <[email protected]
> <javascript:>> 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] <javascript:>.
>> 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/1367c221-0582-4a2b-8d89-c21db06ca7af%40googlegroups.com.
