CollisionCellChoice.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A nearby cell with balanced retained primes

theorem OAI.Ostmann.PublishedProgressionInput.collision_cell_near line 12

Source documentation

The collision estimate and the published ordinary prime interval estimate give a cell near every sufficiently large prescribed center.

theorem PublishedProgressionInput.collision_cell_near (P0 : PublishedProgressionInput) :
    ∃ H : ℝ, ∀ (P : Finset ℕ) (S T : ℕ → Finset ℕ) (μ ν : ℕ → ℕ → ℝ)
      (E target : ℝ), 0 ≤ E → H ≤ target →
      (∀ p ∈ P, p.Prime) →
      (∀ p ∈ P, (S p).Nonempty) → (∀ p ∈ P, (T p).Nonempty) →
      (∀ p ∈ P, (S p).card + (T p).card = p) →
      (∑ p ∈ P, Real.log (p : ℝ) * collisionDefect p (S p) (T p) (μ p) (ν p)) ≤ E →
      (∀ h : ℕ, target ≤ h → (h : ℝ) ≤ target + 64 * E + 1 →
        primeLogCellSet 1 0 h ((h : ℝ) + 1) ⊆ P) →
      ∃ h : ℕ, target ≤ h ∧ (h : ℝ) ≤ target + 64 * E + 1 ∧
        1 / (4 * ((h : ℝ) + 1)) ≤
          ∑ p ∈ primeLogCellSet 1 0 h ((h : ℝ) + 1) \
…

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