I have a hard time locating Theorem 3.2 (b), (c) and (d) of Apostol in Isabelle.
@Manuel Eberl Any idea?
I made a spreadsheet that contains information on where each of the results from Apostol is (it's linked in the paper), but apparently a few of the entries there are wrong…
Thanks. For instance, are you sure mutually_visible_iff
for lattice points is there?
That's another one that I apparently forgot to add to the AFP, but I have it here locally. If you find any others, do tell me and I will add them to the AFP next week.
@Manuel Eberl Arithmetic_Summatory.sum_upto_divisor_sum
may also be missing.
Same possibly for legendre_identity’
of Prime_Number_Theorem
.
@Manuel Eberl Where can I find Apostol's Theorem 4.8 (Shapiro's Tauberian theorem)?
This is basically the shapiro_tauberian
locale here: https://www.isa-afp.org/browser_info/current/AFP/Prime_Distribution_Elementary/Shapiro_Tauberian.html
Anthony Bordg said:
Same possibly for
legendre_identity’
ofPrime_Number_Theorem
.
Have a look at Prime_Distribution_Elementary/More_Dirichlet_Misc.thy:lemma legendre_identity'
Anthony Bordg said:
Manuel Eberl
Arithmetic_Summatory.sum_upto_divisor_sum
may also be missing.
Could that be this?
Prime_Distribution_Elementary/Prime_Distribution_Elementary_Library.thy:lemma sum_upto_divisor_sum1:
Prime_Distribution_Elementary/Prime_Distribution_Elementary_Library.thy:lemma sum_upto_divisor_sum2:
Manuel Eberl said:
Anthony Bordg said:
Manuel Eberl
Arithmetic_Summatory.sum_upto_divisor_sum
may also be missing.Could that be this?
Prime_Distribution_Elementary/Prime_Distribution_Elementary_Library.thy:lemma sum_upto_divisor_sum1: Prime_Distribution_Elementary/Prime_Distribution_Elementary_Library.thy:lemma sum_upto_divisor_sum2:
Looks like sum_upto_divisor_sum1
corresponds to the first equality in Apostol's Theorem 3.11 p.65. But I'm unsure about sum_upto_divisor_sum2
.
okay I'll have a look
Manuel Eberl said:
I made a spreadsheet that contains information on where each of the results from Apostol is (it's linked in the paper), but apparently a few of the entries there are wrong…
For the first theorems of chapter 5, by "library" do you mean HOL-Number_Theory.Cong.thy
?
Should be, yes
the [a = b] (mod c)
notation
the polynomial roots in F_p might also be something in connection with HOL-Algebra
don't quite remember
Oh, also note that chapter 8 is in the AFP as well now (https://www.isa-afp.org/entries/Gauss_Sums.html). Should be fairly complete.
there the theorems are even tagged with their numbers in the book
For Theorem 5.14 for instance Serapis does not know cong_nat_solutions_bij_betw
. So I wonder where it is. Apparently, it's neither in HOL-Number_Theory.Cong.thy
nor in HOL-Algebra.Congruence.thy
using the search function of jedit.
might have been renamed, or I made a mistake
Ah, or I proved this for the book and never moved it to the library. >_>
lemma cong_nat_solutions_bij_betw:
fixes a b n :: nat
defines "d ≡ gcd a n"
assumes "d dvd b" "[a div d * t = b div d] (mod (n div d))" "t < n div d" "n > 0"
shows "bij_betw (λx. (t + x * (n div d)) mod n) {..<d} {x. x < n ∧ [a * x = b] (mod n)}"
I should wait next year now I guess, since the library is probably updated once a year.
The library in isabelle-dev is updated continuously, but the release is only roughly every 9 months. Next one should be in November or October. Sorry for not having been as diligent with these theorems as I should have been!
No worries, it can wait until next October. I just need to make a note of this. In the meantime, there is still a wealth of material to work with.
Are you using this as some kind of training data?
Manuel Eberl said:
Are you using this as some kind of training data?
Yes, that's our hope.
Ah, nice. It's a good thing I made that spreadsheet back then.
@Manuel Eberl I don't find Dirichlet_L.dcharacter.sum_char_divisors_square_ge
and Dirichlet_L.dcharacter.sum_char_divisors_ge
in Dirichlet_L.Dirichlet_Characters.thy
(for Apostol's theorem 6.19). Are these lemmas somewhere else?
Unable to find Dirichlet_L.zorder_Dirichlet_L_principal
(for theorem 12.5).
Same for Dirichlet_L.residue_Dirichlet_L_principal
. Any idea where these theorems are?
Anthony Bordg said:
Manuel Eberl I don't find
Dirichlet_L.dcharacter.sum_char_divisors_square_ge
andDirichlet_L.dcharacter.sum_char_divisors_ge
inDirichlet_L.Dirichlet_Characters.thy
(for Apostol's theorem 6.19). Are these lemmas somewhere else?
Those are in the Dirichlet_L
AFP entry, in the Dirichlet_L_Functions
file.
Having trouble locating bernoulli_even_asymptotics
for Apostol's theorem 12.18.
Likewise for bernpoly_conv_perzeta
for Theorem 12.19.
I assume Zeta_Function.zeta_nonzero_Re_ge_1
is Zeta_Function.zeta_Re_ge_1_nonzero
instead, which seems to roughly correspond to Apostol's theorem 13.6.
Yes, indeed.
Thanks. I'm also assuming that for Apostol's theorem 13.11 by perzeta_one_half
you mean perzeta_one_half_left
.
Yes that looks right
it's quite possible that the names of some of these changed since the time when I made the spreadsheet
most of the other theorems you mentioned are also still lying around in some file that I thought I'd merged into the AFP, but apparently not
For Apostol's theorem 13.13 I assume totient_asymptotics_aux
should be in theory Prime_Distribution_Elementary.PNT_Consequences
, but apparently it's not there.
Do we have Apostol's theorem 's 5.21 (attributed to Lagrange) of his Intro to ANT?
I don't think we have it in that very explicit form, but we have the much more general statement that any nonzero polynomial of degree over a field has at most roots (even taking multiplicity into account). We definitely have this in HOL-Computational_Algebra
and I'm pretty sure we also have it in HOL-Algebra
(I checked at the time).
Getting 5.21 from the HOL-Compuational_Algebra
would be fiddly because it would involve using local type definitions, but getting it from the HOL-Algebra
is straightforward.
@Manuel Eberl Thanks.
Do you know if we have theorems 6.5 and 6.6?
6.5 is just the ord
operation from HOL-Algebra (group.ord
, or just ord
inside the group
locale context).
6.6 should be somewhere in the Subgroup_Adjoin
theory in the Dirichlet_L
AFP entry. However, the approach that Apostol takes is very ad-hoc. I don't like this Subgroup_Adjoin
theory at all and will get rid of it soon.
I had a student working on some theory of (internal) direct products and the fundamental theorem of finitely generated abelian groups. This will supersede a lot of the ad-hoc proofs about characters in my development and make them nicer and more "standard".
The result that corresponds to Apostol's Theorem 6.6 will however still be there, I think.
(Note that the h
in Apostol's 6.6 is currently called subgroup_indicator
– a name inspired by what Apostol calls it, but I couldn't find any reference to this notion in the literature, so I don't think it's standard group theory terminology)
@Manuel Eberl
Regarding stuff about Jacobi symbols (chapter 9), just in case you want to update your document please note that I found them in the AFP (Probabilistic_Prime_tests) but not in the library.
Oh yes, I am aware of that. But it should be moved to the library eventually…
Will put that on my to do list
Last updated: Dec 21 2024 at 16:20 UTC