OAI/NumberTheory/JointDickman/Arithmetic/RegularitySievePrimes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.good_prefix_sieve_set line 13
2. theorem OAI.JointDickman.full_prefix_sieve_set line 30
3. theorem OAI.JointDickman.primePrefix_eq_largePrimeSet line 51
4. theorem OAI.JointDickman.prefix_endpoint_le_sieveCutoff line 82
5. theorem OAI.JointDickman.tilt_prefix_mass_tendsto line 98

   Source documentation

   This is the actual reciprocal mass appearing in the tilted sieve, including its finite cutoff, for every fixed regularity-grid point.

   theorem tilt_prefix_mass_tendsto
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {c g : ℝ}
       (hc : 0 < c) (hc4 : c ≤ 4) (hg : 0 < g) (hg1 : g ≤ 1) :
       Tendsto (fun B : ℕ =>
         tiltPrimeReciprocalMass (auxiliaryCutoff B) (sieveCutoff c B)
           (primePrefix B g (auxiliaryPrimes B)) / auxiliaryLogLength B) atTop (𝓝 g) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.tiltPrimeReciprocalMass, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.sieveCutoff, OAI.JointDickman.primePrefix, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryLogLength

6. theorem OAI.JointDickman.tail_sieve_set line 126
7. theorem OAI.JointDickman.tilt_tail_mass_lower line 157