OAI/NumberTheory/Ostmann/Characters/MixedGiantIdealization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint idealization of the external integer and prime giants

Only the prime coordinate uses a published input. Both error terms below are derived from their original sampling laws, and the Page correction remains inside the prime ideal measure.

  1. theorem OAI.Ostmann.PublishedProgressionInput.mixed_giant_idealization line 19