OAI/NumberTheory/TwoPointCorrelations/HalaszPerronWindowKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A short multiplicative smoothing of Perron's kernel. The difference has both the first-order bound and an integrable inverse-square tail.

  1. def OAI.TwoPointCorrelations.halaszPerronWindowKernel line 13

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPerronWindowKernel.lean:13 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_exp_window_difference line 17

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPerronWindowKernel.lean:17 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_perron_window_factor line 50

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPerronWindowKernel.lean:50 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.halasz_perron_window_bound line 76

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPerronWindowKernel.lean:76 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.halasz_perron_window_tail line 110

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPerronWindowKernel.lean:110 (same declaration text).