(I'll go ahead and "bump" this if no one minds, since it's been a month but
I'm still still going as noted in the last post edits, I better see what my
goal is, and I seem to be spared from that dreaded plague for now. Stay
safe, everyone!)
I tried to see if there was a way to do it just for one point, x/y, to
avoid the function-operation things; that's doomed to failure, but now I
have
|- ( ( ph /\ -. C e. NN0 ) -> ( ( CC _D ( P oF x. ( b e. D |-> ( ( 1 +
b ) ^c -u C ) ) ) ) ` ( B / A ) ) = 0 )
where D is the disk of convergence of radius R (itself 1), P is the
binomial series for ((1+b)^C), C is their exponent r, and B and A are their
x and y, so it's clear the Wikibooks proof is correct. I now know that the
goal is to use dv11cn to prove the equivalence of "( P oF x. ( b e. D |-> (
( 1 + b ) ^c -u C ) ) )" and "( CC X. { 1 } )", and thus of "P" and "( b e.
D |-> ( ( 1 + b ) ^c C ) )"; so some careful rewriting of what I already
have, in terms of function operations, could get me there soon.
I see a light at the end of the tunnel! And that makes me question my
sanity because I'm pretty sure I'm dealing with an *infinite* series. :)
On Thursday, February 27, 2020 at 11:09:35 AM UTC-5, Steve Rodriguez wrote:
>
> 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.
> ―
> Edit 2020-03-07: Welp, that didn't get me too far. The next step for me
> is radcnvrat,
> $( pser.g $)
> radcnvrat.g $e |- G = ( x e. CC |-> ( n e. NN0 |->
> ( ( A ` n ) x. ( x ^ n ) ) ) ) $.
> $( radcnv.a $)
> radcnvrat.a $e |- ( ph -> A : NN0 --> CC ) $.
> $( radcnv.r $)
> radcnvrat.r $e |- R =
> sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
> $.
> radcnvrat.rat $e |- D = ( k e. NN0 |->
> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) ) $.
> radcnvrat.z $e |- Z = ( ZZ>= ` M ) $.
> radcnvrat.m $e |- ( ph -> M e. NN0 ) $.
> radcnvrat.n0 $e |- ( ( ph /\ k e. Z ) -> ( A ` k ) =/= 0 ) $.
> radcnvrat.l $e |- ( ph -> D ~~> L ) $.
> radcnvrat.ln0 $e |- ( ph -> L =/= 0 ) $.
> radcnvrat $p |- ( ph -> R = ( 1 / L ) ) $= ? $.
> With cvgdvgrat I can get
> |- ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) ->
> ( ( ( abs ` x ) x. L ) < 1 <-> seq 0 ( + , ( G ` x ) ) e. dom ~~>
> ) )
> The antecedent becomes (...x e. CC...) if I add the zero case with radcnv0
> <http://us.metamath.org/mpeuni/radcnv0.html>, and with radcnvrat.ln0 it
> becomes
> |- ( ( ( ph /\ x e. CC ) /\ ( abs ` x ) =/= ( 1 / L ) ) ->
> ( ( abs ` x ) < ( 1 / L ) <-> seq 0 ( + , ( G ` x ) ) e. dom ~~>
> ) )
> or
> |- ( ( ph /\ x e. CC ) ->
> ( ( ( abs ` x ) < ( 1 / L ) -> seq 0 ( + , ( G ` x ) ) e. dom ~~>
> ) /\
> ( seq 0 ( + , ( G ` x ) ) e. dom ~~> -> -. ( 1 / L ) < ( abs `
> x ) ) ) )
> To me that's exactly what Wikipedia's ROC proof sketch is going for, but
> to be sure of that (and make it usable with pserdv2) I think I need to
> match it up with a supremum theorem like eqsup, eqsupd, supxr, or supxr2
> that allows for the sup not necessarily being a member of { r e. RR | ...
> }. It's obvious to me that 1/L is the sup—1/L is not necessarily a member
> of the convergence region, but no member is greater in absolute value than
> 1/L and any y even infinitesimally smaller than 1/L has members of the
> region sandwiched between y and 1/L—but I can't quite make the mental and
> mechanical (metamathechanical?) connection, even though it *feels* like
> it'd be just another case of Mario's proof sketch in the first reply or
> suchlike. (Changing "( G ` x )" to "( G ` ( abs ` x ) )" by way of the
> idempotence of abs doesn't quite get me closer, but would help in changing
> all the "( abs ` x )"es to "y"...)
> ―
> Edit 2020-03-08: Found another path to get radcnvrat done. Verifying now
> and submitting soon.
> ―
> Edit 2020-03-15: Still going. I split the binomial-series proof in two.
> The case for nonnegative-integer exponents is done; it needed a cvgcmpce to
> show convergence of the series so that I could isumsplit
> <http://us.metamath.org/mpeuni/isumsplit.html> the sum over NN0 into the
> finite sum of binom and the zeroes after that, but it was easy besides.
> I'll hold off on submitting until I've proven (more of) the
> non-nonnegative-integer case; I am just past getting the derivative of the
> series in the proof
> <https://en.wikibooks.org/wiki/Advanced_Calculus/Newton%27s_general_binomial_theorem>
>
> and splitting off that "e. NN0" case made verifying the ratio in the ROC
> part easier. It'll require SF's mathboxed FallFac
> <http://us.metamath.org/mpeuni/df-fallfac.html> and prod_
> <http://us.metamath.org/mpeuni/df-prod.html>, and I'm mulling whether to
> also use oFC <http://us.metamath.org/mpeuni/df-ofc.html> (and whether to
> redo expgrowth, done ~2 years before that arrived, with that...) or plain
> oF <http://us.metamath.org/mpeuni/df-of.html>, for multiplying functions
> and such.
>
> 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]>
>> 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/ac40b522-c552-4fee-9a34-a4ab99eddd37%40googlegroups.com.
