OAI/NumberTheory/JointDickman/Arithmetic/SieveSingleDensity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.sievePrimes line 13
2. def OAI.JointDickman.roughSieveTheta line 15
3. def OAI.JointDickman.roughSieveRate line 17
4. theorem OAI.JointDickman.roughSieveTheta_bounds line 19
5. theorem OAI.JointDickman.roughSieveRate_bounds line 24
6. theorem OAI.JointDickman.roughSieveRate_sum line 36
7. theorem OAI.JointDickman.roughSieveRate_removed_le line 56
8. def OAI.JointDickman.roughSieveDensity line 76
9. theorem OAI.JointDickman.roughSieveDensity_log_bound line 81

   Source documentation

   The square of the one-form density has exactly the required two logarithms in its denominator; bounded primes have already been removed.

   theorem roughSieveDensity_log_bound
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ C : ℝ, 0 < C ∧ ∀ P Z : ℕ, 2 ≤ P → P ≤ Z →
         roughSieveDensity P Z ^ 2 * Real.log P * Real.log Z ≤ C := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.roughSieveDensity