PrimePool.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.eventually_prime_count_lower line 11
Source documentation
A coarse elementary lower estimate for the prime counting function.
```
theorem eventually_prime_count_lower :
    ∀ᶠ x : ℝ in atTop, x / (4 * Real.log x) ≤ (Nat.primeCounting ⌊x⌋₊ : ℝ) := by
…
```
theorem OAI.Problem337.eventually_prime_count_upper line 37
Source documentation
A coarse elementary upper estimate for the prime counting function.
```
theorem eventually_prime_count_upper :
    ∀ᶠ x : ℝ in atTop, (Nat.primeCounting ⌊x⌋₊ : ℝ) ≤ 5 * x / Real.log x := by
…
```
def OAI.Problem337.widePrimePool line 70
Source documentation
A prime pool in a fixed-width multiplicative interval.
```
def widePrimePool (x : ℝ) : Finset ℕ :=
…
```
theorem OAI.Problem337.eventually_wide_prime_pool_large line 73
theorem OAI.Problem337.eventually_residue_prime_pool_large line 102
Source documentation
The residue construction needs polynomially many primes at scale S^100. Chebyshev's elementary estimates suffice if the fixed interval width is 64.
```
theorem eventually_residue_prime_pool_large :
    ∀ᶠ S : ℝ in atTop,
      S ^ 99 ≤ ((widePrimePool (S ^ 100)).card : ℝ) := by
…
```
Mentions: OAI.Problem337.widePrimePool
theorem OAI.Problem337.mem_widePrimePool_iff line 126
Source documentation
Membership records the exact real endpoints, without rounding ambiguity.
```
theorem mem_widePrimePool_iff {x : ℝ} (hx : 0 ≤ x) {p : ℕ} :
    p ∈ widePrimePool x ↔ Nat.Prime p ∧ x < (p : ℝ) ∧ (p : ℝ) ≤ 64 * x := by
…
```
Mentions: OAI.Problem337.widePrimePool

theorem OAI.Problem337.eventually_residue_prime_pool_spec line 138

Source documentation

Full elementary prime-pool interface for the residue construction.

theorem eventually_residue_prime_pool_spec :
    ∀ᶠ S : ℝ in atTop,
      S ^ 99 ≤ ((widePrimePool (S ^ 100)).card : ℝ) ∧
      ∀ p ∈ widePrimePool (S ^ 100),
        Nat.Prime p ∧ S ^ 100 < (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101 := by
…

Mentions: OAI.Problem337.widePrimePool