WholePrimeGrid.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact short-cell partitions of the original whole prime shells

def OAI.Ostmann.wholePrimeGridCount line 12
theorem OAI.Ostmann.wholePrimeGridCount_pos line 14
theorem OAI.Ostmann.wholePrimeGridCount_upper line 18
theorem OAI.Ostmann.wholePrimeGridCount_width line 25
theorem OAI.Ostmann.interval_grid_width line 33
theorem OAI.Ostmann.whole_prime_grid_support line 45
Source documentation
The mesh covers the entire original shell, including every boundary prime allowed by its left-open, right-closed convention.
```
theorem whole_prime_grid_support (q : ℕ) [NeZero q] (a b : ℝ)
    (hab : a ≤ b) (hq : (q : ℝ) ≤ Real.exp (Real.exp a)) :
    let N := wholePrimeGridCount b
…
```
Mentions: OAI.Ostmann.wholePrimeGridCount
theorem OAI.Ostmann.whole_interval_prime_grid_support line 63
Source documentation
A whole shell of arbitrary log-log width has the same exact finite grid. The mesh size depends on the upper endpoint, not on a unit-width restriction.
```
theorem whole_interval_prime_grid_support (q : ℕ) [NeZero q] (a b : ℝ)
    (hab : a ≤ b) (hq : (q : ℝ) ≤ Real.exp (Real.exp a)) :
    let N := wholePrimeGridCount b
…
```
Mentions: OAI.Ostmann.wholePrimeGridCount
theorem OAI.Ostmann.wholePrimeGridCount_eventual line 87
Source documentation
The coarse partition is enough because the sharp real kernel is integrated exactly on each cell. Its count is far below the cell budget.
```
theorem wholePrimeGridCount_eventual (K : ℝ) (hK : 0 ≤ K) :
    ∀ᶠ L : ℝ in atTop, ∀ b : ℝ, b ≤ K * L →
      (wholePrimeGridCount b : ℝ) ≤ Real.exp (Real.exp ((14 / 10000 : ℝ) * L)) := by
…
```
Mentions: OAI.Ostmann.wholePrimeGridCount