OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronInversion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Triangular Perron inversion from Mellin inversion. The triangular function is a difference of two elementary Mellin transforms.

  1. def OAI.TwoPointCorrelations.modFiveTriangle line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronInversion.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFiveTriangle_hasMellin line 16

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

  3. lemma OAI.TwoPointCorrelations.modFiveTriangle_continuous line 50

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronInversion.lean:52 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFiveTriangle_verticalIntegrable line 54

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronInversion.lean:56 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.modFivePerron_inversion line 63

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronInversion.lean:65 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFivePerron_gt_one line 90

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronInversion.lean:92 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.modFivePerron_lt_one line 98

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronInversion.lean:100 (same declaration text).