OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronParameters.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Elementary parameter choices for the smoothed Perron bound. The height is exp(y) and the original cutoff is exp(y²).

  1. lemma OAI.TwoPointCorrelations.modFive_perron_height line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronParameters.lean:13 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFive_perron_right_power line 25

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronParameters.lean:25 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFive_perron_left_power line 31

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronParameters.lean:31 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFive_perron_polynomial_absorption line 42

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronParameters.lean:42 (same declaration text).