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.
