OAI/NumberTheory/TwoPointCorrelations/HalaszDistanceDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The elementary losses when changing the prime cutoff by a fixed power.

  1. lemma OAI.TwoPointCorrelations.halasz_decay_shift line 9

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDistanceDecay.lean:9 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_log_error_cutoff line 31

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDistanceDecay.lean:31 (same declaration text).