OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimeOscillation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The moderate-frequency prime-phase step in MRT Lemma A.4. The frequency dependence of partial summation is explicit, so a growing frequency range can be paid for by the exponential prime-number error.

  1. lemma OAI.TwoPointCorrelations.halasz_oscillatory_weight_bounds line 15

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeOscillation.lean:15 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.halasz_oscillatory_theta_error line 45

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeOscillation.lean:45 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_cosine_defect line 73

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeOscillation.lean:73 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_prime_cosine_defect line 80

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeOscillation.lean:80 (same declaration text).