OAI/NumberTheory/TwoPointCorrelations/ModFivePerronInversion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Triangular Perron inversion from Mathlib's proved Mellin inversion. The triangular function is a difference of two elementary Mellin transforms; no additional analytic input or dependency source is needed.

  1. def OAI.TwoPointCorrelations.modFiveTriangle line 15

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronInversion.lean:13 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFiveTriangle_hasMellin line 18

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

  3. lemma OAI.TwoPointCorrelations.modFiveTriangle_continuous line 52

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronInversion.lean:50 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFiveTriangle_verticalIntegrable line 56

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronInversion.lean:54 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.modFivePerron_inversion line 65

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronInversion.lean:63 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFivePerron_gt_one line 92

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronInversion.lean:90 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.modFivePerron_lt_one line 100

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronInversion.lean:98 (same declaration text).