OAI/NumberTheory/TwoPoint/Halasz/HalaszWindowIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The central part of the prime--prime--smooth Perron integral. The first prime factor uses its ordinary mean square and the second its global Cauchy-weighted mean square.

  1. lemma OAI.TwoPointCorrelations.halasz_vertical_norm line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszWindowIntegral.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_window_middle_bound line 20

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszWindowIntegral.lean:20 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.halasz_prime_window_middle line 52

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