PrimeLogCellMeans.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual prime log cells and their means

def OAI.Ostmann.primeLogIndex line 15
Source documentation
The cell (h,h+1] containing the logarithm of a prime.
```
noncomputable def primeLogIndex (p : ℕ) : ℕ := ⌈Real.log (p : ℝ)⌉₊ - 1
```
theorem OAI.Ostmann.primeLogIndex_bounds line 17
theorem OAI.Ostmann.primeLogIndex_cell line 39

theorem OAI.Ostmann.PublishedProgressionInput.primeLogIndex_mass_bound line 46

Source documentation

The actual prime fibers obey the uniform cell cap used in good-cell selection.

theorem PublishedProgressionInput.primeLogIndex_mass_bound (P0 : PublishedProgressionInput) :
    ∀ᶠ B : ℝ in atTop, ∀ (P : Finset ℕ), (∀ p ∈ P, p.Prime) →
      ∀ h : ℕ, B ≤ h →
      finiteCellMass P primeLogIndex (fun p => (p : ℝ)⁻¹) h ≤ 2 / B := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.finiteCellMass, OAI.Ostmann.primeLogIndex