OAI/NumberTheory/Ostmann/Construction/PrimeLogCellMeasure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Ostmann.finite_primeLogAtom line 13
2. def OAI.Ostmann.primeLogCellMeasure line 17
3. instance OAI.Ostmann.finite_primeLogCellMeasure line 20
4. theorem OAI.Ostmann.primeLogCellMeasure_integral line 25
5. theorem OAI.Ostmann.primeLogCellMeasure_mass line 38
6. theorem OAI.Ostmann.PublishedProgressionInput.primeLogCellMeasure_mass_eventually line 47

   Source documentation

   All residue classes and shorter cells obey the same eventual mass bound.

   theorem PublishedProgressionInput.primeLogCellMeasure_mass_eventually (P : PublishedProgressionInput) :
       ∀ᶠ u : ℝ in atTop, ∀ q a : ℕ, ∀ v : ℝ, v ≤ u + 1 →
         (primeLogCellMeasure q a u v).real Set.univ ≤ 2 := by
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.primeLogCellMeasure