RichGridShell.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Whole rich unit shells on one fixed grid

theorem OAI.Ostmann.exists_rich_grid_shell line 11

theorem OAI.Ostmann.exists_rich_prime_grid_block line 68

Source documentation

The upper-block selection in the character argument, including whole rich unit shells from the single grid based at the selected left endpoint.

theorem exists_rich_prime_grid_block {C : ℝ} (hMertens : MertensEstimate C)
    (M : ℕ) (hM : 0 < M) (d ε : ℝ) (hd : 0 < d) (hε : 0 < ε)
    (hmesh : 20 ≤ ε * M) :
    ∃ H : ℕ, ∀ (K : ℕ), 1 ≤ K → 4 ≤ ε * K →
      64 * (Real.exp 1 + 1) ≤ d * ε * 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 ∧
…

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