RichPrimeCellTargets.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Target words in a rich shell of actual primes

theorem OAI.Ostmann.PublishedProgressionInput.rich_prime_cell_targets line 14

Source documentation

A shell of positive harmonic mass and positive mean supplies heavy cells whose ordered indices approximate every sufficiently large target.

theorem PublishedProgressionInput.rich_prime_cell_targets
    (P0 : PublishedProgressionInput) (c δ : ℝ) (hc : 0 < c) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℝ in atTop, ∀ (P : Finset ℕ) (f : ℕ → ℝ),
      (∀ p ∈ P, p.Prime) →
      (∀ p ∈ P, B ≤ primeLogIndex p ∧ (primeLogIndex p : ℝ) ≤ 3 * B) →
      (∀ p ∈ P, f p ≤ 1) → c ≤ ∑ p ∈ P, (p : ℝ)⁻¹ →
      δ * (∑ p ∈ P, (p : ℝ)⁻¹) ≤ ∑ p ∈ P, (p : ℝ)⁻¹ * f p →
      ∀ T : ℝ, C * B ≤ T → ∃ (n : ℕ) (w : List ℕ),
        w.length = n ∧
        (∀ h ∈ w,
          δ * c / (32 * B) ≤ finiteCellMass P primeLogIndex (fun p => (p : ℝ)⁻¹) h ∧
          δ / 2 ≤ finiteCellMean P primeLogIndex (fun p => (p : ℝ)⁻¹) f h) ∧
…

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