OAI/NumberTheory/TwoPoint/Fourier/ModFiveContourKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Elementary kernel estimates for the finite Perron rectangle. The vertical side has an integrable quadratic majorant, while each horizontal side has the explicit inverse-square height saving.

  1. def OAI.TwoPointCorrelations.modFivePerronKernel line 18

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveContourKernel.lean:18 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFive_perron_denominator_vertical line 21

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveContourKernel.lean:21 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFive_perron_denominator_horizontal line 42

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

  4. lemma OAI.TwoPointCorrelations.modFive_perron_kernel_vertical line 51

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveContourKernel.lean:51 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.modFive_perron_kernel_horizontal line 62

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveContourKernel.lean:62 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFivePerronKernel_integrable line 71

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveContourKernel.lean:71 (same declaration text).