OAI/NumberTheory/Ostmann/Construction/PrimeLogCellUpper.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform upper mass bound on a logarithmic prime cell

  1. theorem OAI.Ostmann.log_unit_ratio_upper line 13
  2. theorem OAI.Ostmann.PublishedProgressionInput.ordinary_interval_upper line 19
  3. theorem OAI.Ostmann.sum_primeLogCellSet_reciprocal line 32
  4. theorem OAI.Ostmann.PublishedProgressionInput.prime_log_cell_upper line 39

    Source documentation

    Every subset of the actual prime cell has reciprocal mass O(1/s), uniformly in the subset.

    theorem PublishedProgressionInput.prime_log_cell_upper (P : PublishedProgressionInput) :
    ∀ᶠ s : ℝ in atTop, ∀ E : Finset ℕ,
      E ⊆ primeLogCellSet 1 0 s (s + 1) → (∑ p ∈ E, (p : ℝ)⁻¹) ≤ 2 / s := by
…

    Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.primeLogCellSet