PrimeProductGrowth.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.eventually_primeCounting_ge_linear_div_log line 13
Source documentation
Chebyshev's elementary bounds give the lower prime-density estimate needed for the size of the first-prime product. No prime number theorem is used.
```
lemma eventually_primeCounting_ge_linear_div_log :
    ∀ᶠ x : ℝ in atTop,
      (Real.log 2 / 2) * x / Real.log x ≤ (Nat.primeCounting ⌊x⌋₊ : ℝ) := by
…
```
lemma OAI.Problem337.eventually_nth_prime_le_rpow line 30
lemma OAI.Problem337.primePrefixProduct_dvd_of_le line 66
lemma OAI.Problem337.eventually_log_primePrefixProduct_le_growth line 72
Source documentation
The sharp leading coefficient in the logarithm of a prime-prefix product needs only Chebyshev's lower prime-counting estimate.
```
lemma eventually_log_primePrefixProduct_le_growth (δ : ℝ) (hδ : 0 < δ) :
    ∀ᶠ n : ℕ in atTop,
      Real.log (primePrefixProduct n : ℝ) ≤ (1 + δ) * (n : ℝ) * Real.log (n : ℝ) := by
…
```
Mentions: OAI.Problem337.primePrefixProduct
lemma OAI.Problem337.tendsto_log_natCeil_mul_div_log line 96
lemma OAI.Problem337.eventually_log_primePrefixProduct_ceil_le line 113
Source documentation
A directly usable prime-product bound at the logarithmic number of primes required by rational-divisor supply.
```
lemma eventually_log_primePrefixProduct_ceil_le (A ε : ℝ) (hA : 0 < A) (hε : 0 < ε) :
    ∀ᶠ x : ℝ in atTop,
      Real.log (primePrefixProduct ⌈A * x⌉₊ : ℝ) ≤ (A + ε) * x * Real.log x := by
…
```
Mentions: OAI.Problem337.primePrefixProduct
lemma OAI.Problem337.log_factorial_natFloor_le_sq line 140
def OAI.Problem337.markedSupplyMultiplier line 152
Source documentation
The supply multiplier from the marked-denominator construction, with the prime count already simplified using log (m^4) = 4 log m.
```
def markedSupplyMultiplier (m : ℕ) : ℕ :=
…
```
lemma OAI.Problem337.markedSupplyMultiplier_pos line 156
lemma OAI.Problem337.eventually_log_markedSupplyMultiplier_le line 159
lemma OAI.Problem337.lt_markedSupplyMultiplier line 194