OAI/NumberTheory/TwoPointCorrelations/ModFiveRectangleShift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact finite rectangle shift, with an explicit horizontal cost. All functions are complex scalar functions, as needed for the three fixed nonprincipal Dirichlet L-functions.

  1. lemma OAI.TwoPointCorrelations.modFive_rectangle_shift line 14

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveRectangleShift.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFive_rectangle_shift_bound line 26

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveRectangleShift.lean:26 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFive_vertical_quadratic_bound line 52

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveRectangleShift.lean:52 (same declaration text).