OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Continuity and uniform bounds for the actual smooth Euler series on the Perron line. Only values at positive integers are bounded.

  1. lemma OAI.TwoPointCorrelations.halasz_distance_nonneg line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszSmoothBounds.lean:13 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_smooth_line_continuous line 24

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszSmoothBounds.lean:24 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.halasz_smooth_uniform_bound line 44

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszSmoothBounds.lean:44 (same declaration text).