Anthony Bordg (Apr 29 2021 at 21:38): Anthony Bordg (Apr 29 2021 at 21:38):I have a hard time locating Theorem 3.2 (b), (c) and (d) of Apostol in Isabelle.
@Manuel Eberl Any idea?
Manuel Eberl (Apr 30 2021 at 07:37): Manuel Eberl (Apr 30 2021 at 07:37):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…
Anthony Bordg (Apr 30 2021 at 14:44):Thanks. For instance, are you sure mutually_visible_iff for lattice points is there?
Manuel Eberl (Apr 30 2021 at 15:38):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.
Anthony Bordg (May 01 2021 at 10:01):@Manuel Eberl Arithmetic_Summatory.sum_upto_divisor_sum may also be missing.
Anthony Bordg (May 01 2021 at 10:24):Same possibly for legendre_identity’ of Prime_Number_Theorem.
Anthony Bordg (May 03 2021 at 15:28):@Manuel Eberl Where can I find Apostol's Theorem 4.8 (Shapiro's Tauberian theorem)?
Manuel Eberl (May 03 2021 at 15:29):This is basically the shapiro_tauberian locale here: https://www.isa-afp.org/browser_info/current/AFP/Prime_Distribution_Elementary/Shapiro_Tauberian.html
Manuel Eberl (May 03 2021 at 15:31):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'
Manuel Eberl (May 03 2021 at 15:32):Anthony Bordg said:
Manuel Eberl
Arithmetic_Summatory.sum_upto_divisor_summay 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_summay 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.
Manuel Eberl (May 03 2021 at 16:13):okay I'll have a look
Anthony Bordg (May 07 2021 at 10:06):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?
Manuel Eberl (May 07 2021 at 10:07):Should be, yes
Manuel Eberl (May 07 2021 at 10:08):the [a = b] (mod c) notation
Manuel Eberl (May 07 2021 at 10:09):the polynomial roots in F_p might also be something in connection with HOL-Algebra
Manuel Eberl (May 07 2021 at 10:09):don't quite remember
Manuel Eberl (May 07 2021 at 10:10):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.
Manuel Eberl (May 07 2021 at 10:11):there the theorems are even tagged with their numbers in the book
Anthony Bordg (May 07 2021 at 10:18):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.
Manuel Eberl (May 07 2021 at 10:25):might have been renamed, or I made a mistake
Manuel Eberl (May 07 2021 at 10:26):Ah, or I proved this for the book and never moved it to the library. >_>
Manuel Eberl (May 07 2021 at 10:26):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.
Manuel Eberl (May 07 2021 at 12:48):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!
Anthony Bordg (May 07 2021 at 13:32):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.
Manuel Eberl (May 07 2021 at 13:33):Are you using this as some kind of training data?
Anthony Bordg (May 07 2021 at 13:38):Manuel Eberl said:
Are you using this as some kind of training data?
Yes, that's our hope.
Manuel Eberl (May 07 2021 at 13:40):Ah, nice. It's a good thing I made that spreadsheet back then.
Anthony Bordg (May 10 2021 at 11:22):@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?
Anthony Bordg (May 17 2021 at 11:00):Unable to find Dirichlet_L.zorder_Dirichlet_L_principal (for theorem 12.5).
Anthony Bordg (May 17 2021 at 11:05):Same for Dirichlet_L.residue_Dirichlet_L_principal. Any idea where these theorems are?
Manuel Eberl (May 17 2021 at 11:06):Anthony Bordg said:
Manuel Eberl I don't find
Dirichlet_L.dcharacter.sum_char_divisors_square_geandDirichlet_L.dcharacter.sum_char_divisors_geinDirichlet_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.
Anthony Bordg (May 18 2021 at 10:38):Having trouble locating bernoulli_even_asymptotics for Apostol's theorem 12.18.
Anthony Bordg (May 18 2021 at 10:46):Likewise for bernpoly_conv_perzeta for Theorem 12.19.
Anthony Bordg (May 19 2021 at 09:14):I assume Zeta_Function.zeta_nonzero_Re_ge_1 is Zeta_Function.zeta_Re_ge_1_nonzeroinstead, which seems to roughly correspond to Apostol's theorem 13.6.
Manuel Eberl (May 19 2021 at 09:28):Yes, indeed.
Anthony Bordg (May 19 2021 at 09:39):Thanks. I'm also assuming that for Apostol's theorem 13.11 by perzeta_one_half you mean perzeta_one_half_left.
Manuel Eberl (May 19 2021 at 09:45):Yes that looks right
Manuel Eberl (May 19 2021 at 09:46):it's quite possible that the names of some of these changed since the time when I made the spreadsheet
Manuel Eberl (May 19 2021 at 09:46):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
Anthony Bordg (May 19 2021 at 10:15):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.
Anthony Bordg (Jun 10 2021 at 10:10):Do we have Apostol's theorem 's 5.21 (attributed to Lagrange) of his Intro to ANT?
Manuel Eberl (Jun 10 2021 at 10:15):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.
Anthony Bordg (Jun 10 2021 at 16:43):@Manuel Eberl Thanks.
Do you know if we have theorems 6.5 and 6.6?
Manuel Eberl (Jun 10 2021 at 19:51):6.5 is just the ord operation from HOL-Algebra (group.ord, or just ord inside the group locale context).
Manuel Eberl (Jun 10 2021 at 19:55):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.
Manuel Eberl (Jun 10 2021 at 19:56):(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)
Anthony Bordg (Jun 11 2021 at 16:47):@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.
Manuel Eberl (Jun 11 2021 at 18:00):Oh yes, I am aware of that. But it should be moved to the library eventually…
Manuel Eberl (Jun 11 2021 at 18:00):Will put that on my to do list
Last updated: Apr 25 2024 at 01:08 UTC