OAI/NumberTheory/TwoPoint/Bounds/OscillatoryThetaError.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform partial summation for (1-cos(t log p))/p, with |t|≤2. The oscillatory prime estimate is deduced from the theta error.

  1. def OAI.TwoPointCorrelations.oscillatoryReciprocalLog line 15

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

  2. lemma OAI.TwoPointCorrelations.reciprocalLog_size line 18

    Also declared: OAI/NumberTheory/TwoPointCorrelations/OscillatoryThetaError.lean:18 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.reciprocalLog_deriv_size line 28

    Also declared: OAI/NumberTheory/TwoPointCorrelations/OscillatoryThetaError.lean:28 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.oscillatoryReciprocalLog_hasDerivAt line 41

    Also declared: OAI/NumberTheory/TwoPointCorrelations/OscillatoryThetaError.lean:41 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.oscillatoryReciprocalLog_bounds line 55

    Also declared: OAI/NumberTheory/TwoPointCorrelations/OscillatoryThetaError.lean:55 (same declaration text).

  6. theorem OAI.TwoPointCorrelations.oscillatory_theta_error line 83

    Also declared: OAI/NumberTheory/TwoPointCorrelations/OscillatoryThetaError.lean:83 (same declaration text).