OAI/NumberTheory/TwoPointCorrelations/ModFiveSmoothedPsi.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact triangular Perron formula for the twisted von Mangoldt sums. Nonintegral real cutoffs avoid the irrelevant boundary value of the scalar kernel; later we use half-integral cutoffs to recover every integer sum.

  1. def OAI.TwoPointCorrelations.modFiveSmoothedPsi line 16

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveSmoothedPsi.lean:16 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.modFivePerron_finite_sum line 20

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveSmoothedPsi.lean:20 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.modFiveSmoothedPsi_perron line 49

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveSmoothedPsi.lean:49 (same declaration text).