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’`

of`Prime_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`

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?

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 $n$ over a field has at most $n$ 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: Feb 27 2024 at 08:17 UTC