Stream: Is there code for X?

Topic: asymptotic formulas


view this post on Zulip 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?

view this post on Zulip Manuel Eberl (Apr 30 2021 at 07:37):

See here: https://www.isa-afp.org/browser_info/current/AFP/Prime_Distribution_Elementary/Partial_Zeta_Bounds.html

view this post on Zulip 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…

view this post on Zulip Anthony Bordg (Apr 30 2021 at 14:44):

Thanks. For instance, are you sure mutually_visible_iff for lattice points is there?

view this post on Zulip 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.

view this post on Zulip Anthony Bordg (May 01 2021 at 10:01):

@Manuel Eberl Arithmetic_Summatory.sum_upto_divisor_sum may also be missing.

view this post on Zulip Anthony Bordg (May 01 2021 at 10:24):

Same possibly for legendre_identity’ of Prime_Number_Theorem.

view this post on Zulip Anthony Bordg (May 03 2021 at 15:28):

@Manuel Eberl Where can I find Apostol's Theorem 4.8 (Shapiro's Tauberian theorem)?

view this post on Zulip 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

view this post on Zulip Manuel Eberl (May 03 2021 at 15:31):

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'

view this post on Zulip Manuel Eberl (May 03 2021 at 15:32):

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:

view this post on Zulip Anthony Bordg (May 03 2021 at 16:12):

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.

view this post on Zulip Manuel Eberl (May 03 2021 at 16:13):

okay I'll have a look

view this post on Zulip 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?

view this post on Zulip Manuel Eberl (May 07 2021 at 10:07):

Should be, yes

view this post on Zulip Manuel Eberl (May 07 2021 at 10:08):

the [a = b] (mod c) notation

view this post on Zulip Manuel Eberl (May 07 2021 at 10:09):

the polynomial roots in F_p might also be something in connection with HOL-Algebra

view this post on Zulip Manuel Eberl (May 07 2021 at 10:09):

don't quite remember

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (May 07 2021 at 10:11):

there the theorems are even tagged with their numbers in the book

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (May 07 2021 at 10:25):

might have been renamed, or I made a mistake

view this post on Zulip Manuel Eberl (May 07 2021 at 10:26):

Ah, or I proved this for the book and never moved it to the library. >_>

view this post on Zulip 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)}"

view this post on Zulip Anthony Bordg (May 07 2021 at 11:25):

I should wait next year now I guess, since the library is probably updated once a year.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (May 07 2021 at 13:33):

Are you using this as some kind of training data?

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (May 07 2021 at 13:40):

Ah, nice. It's a good thing I made that spreadsheet back then.

view this post on Zulip 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?

view this post on Zulip Anthony Bordg (May 17 2021 at 11:00):

Unable to find Dirichlet_L.zorder_Dirichlet_L_principal (for theorem 12.5).

view this post on Zulip Anthony Bordg (May 17 2021 at 11:05):

Same for Dirichlet_L.residue_Dirichlet_L_principal. Any idea where these theorems are?

view this post on Zulip Manuel Eberl (May 17 2021 at 11:06):

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.

view this post on Zulip Anthony Bordg (May 18 2021 at 10:38):

Having trouble locating bernoulli_even_asymptotics for Apostol's theorem 12.18.

view this post on Zulip Anthony Bordg (May 18 2021 at 10:46):

Likewise for bernpoly_conv_perzeta for Theorem 12.19.

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (May 19 2021 at 09:28):

Yes, indeed.

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (May 19 2021 at 09:45):

Yes that looks right

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 nn over a field has at most nn 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.

view this post on Zulip Anthony Bordg (Jun 10 2021 at 16:43):

@Manuel Eberl Thanks.
Do you know if we have theorems 6.5 and 6.6?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (Jun 11 2021 at 18:00):

Oh yes, I am aware of that. But it should be moved to the library eventually…

view this post on Zulip Manuel Eberl (Jun 11 2021 at 18:00):

Will put that on my to do list


Last updated: Feb 27 2024 at 08:17 UTC