PrimeRichBlock.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A rich upper block with finitely many possible scales

theorem OAI.Ostmann.exists_prime_rich_block line 13

Source documentation

The number of density increments depends on the initial density and subdivision ratio, and is independent of the requested minimum block scale.

theorem exists_prime_rich_block {C : ℝ} (hMertens : MertensEstimate C)
    (M : ℕ) (hM : 0 < M) (d : ℝ) (hd : 0 < d) :
    ∃ H : ℕ, ∀ (K : ℕ), 1 ≤ K → ∀ (P : Finset ℕ), (∀ p ∈ P, p.Prime) →
      ∀ a : ℝ, max C 0 ≤ a →
      d * (5 * K * (M : ℝ) ^ H) ≤
        weightedIntervalMass P (fun p => Real.log (Real.log p)) (fun p => (p : ℝ)⁻¹)
          a (a + 5 * K * (M : ℝ) ^ H) →
      ∃ (j : ℕ) (U : ℝ), j ≤ H ∧ a ≤ U ∧
        U + 5 * K * (M : ℝ) ^ j ≤ a + 5 * K * (M : ℝ) ^ H ∧
        ∀ u v : ℝ, U ≤ u → u ≤ v → v ≤ U + 5 * K * (M : ℝ) ^ j →
          4 * (5 * K * (M : ℝ) ^ j / M) ≤ v - u →
          (d / 4) * (v - u) ≤
…

Mentions: OAI.Ostmann.MertensEstimate, OAI.Ostmann.weightedIntervalMass

theorem OAI.Ostmann.exists_rich_prime_subblock line 86

Source documentation

The selected block comes from the original long prime interval; a positive-density starting block is constructed by averaging.

theorem exists_rich_prime_subblock {C : ℝ} (hMertens : MertensEstimate C)
    (M : ℕ) (hM : 0 < M) (d : ℝ) (hd : 0 < d) :
    ∃ H : ℕ, ∀ (K : ℕ), 1 ≤ K → ∀ (P : Finset ℕ), (∀ p ∈ P, p.Prime) →
      ∀ a L : ℝ, max C 0 ≤ a → 0 ≤ L →
      2 * (Real.exp 1 + 1) * (5 * K * (M : ℝ) ^ H + 1) < d * L →
      d * L ≤ weightedIntervalMass P (fun p => Real.log (Real.log p))
        (fun p => (p : ℝ)⁻¹) a (a + L) →
      ∃ (j : ℕ) (U : ℝ), j ≤ H ∧ a ≤ U ∧
        U + 5 * K * (M : ℝ) ^ j ≤ a + L ∧
        ∀ u v : ℝ, U ≤ u → u ≤ v → v ≤ U + 5 * K * (M : ℝ) ^ j →
          4 * (5 * K * (M : ℝ) ^ j / M) ≤ v - u →
          (d / 8) * (v - u) ≤
…

Mentions: OAI.Ostmann.MertensEstimate, OAI.Ostmann.weightedIntervalMass