OAI/NumberTheory/TwoPointCorrelations/ModFiveAbelBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Uniform Abel-integral estimates for the nonprincipal modulus-five characters. The integral converges throughout re s > 0; its norm is at most 4 * ‖s‖ / re s, using the exact period bound rather than a new input.

  1. def OAI.TwoPointCorrelations.modFiveSummatory line 17

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelBounds.lean:17 (same declaration text).

  2. def OAI.TwoPointCorrelations.modFiveAbelKernel line 20

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

  3. def OAI.TwoPointCorrelations.modFiveAbelIntegral line 23

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelBounds.lean:23 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFiveSummatory_measurable line 26

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

  5. lemma OAI.TwoPointCorrelations.modFiveSummatory_norm line 31

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelBounds.lean:31 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFiveAbelKernel_measurable line 35

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelBounds.lean:35 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.modFiveAbelKernel_norm_le line 44

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelBounds.lean:44 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.modFiveAbelKernel_integrable line 53

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelBounds.lean:53 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.modFiveAbelKernel_integral_norm line 62

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelBounds.lean:62 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.modFiveAbelIntegral_norm line 77

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelBounds.lean:77 (same declaration text).

  11. theorem OAI.TwoPointCorrelations.modFiveAbelIntegral_eq_LFunction line 86

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelBounds.lean:86 (same declaration text).