OAI/NumberTheory/TwoPointCorrelations/HalaszWindowPerron.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact inversion for the narrow Perron window. Absolute convergence on the line is enough, including the smooth Euler series at real part one.

  1. lemma OAI.TwoPointCorrelations.halasz_LSeries_line_continuous line 14

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszWindowPerron.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_LSeries_line_bound line 32

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszWindowPerron.lean:32 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_LSeries_perron_integrable line 38

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszWindowPerron.lean:38 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_LSeries_window_integrable line 52

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszWindowPerron.lean:52 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.halasz_window_perron line 66

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszWindowPerron.lean:66 (same declaration text).

  6. theorem OAI.TwoPointCorrelations.halasz_window_unsmoothing line 91

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszWindowPerron.lean:91 (same declaration text).