PrimeTripleAsymptotics.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.eventually_log_pow_lt_mul_rpow line 12
Source documentation
Any fixed logarithmic power is eventually smaller than an arbitrary positive multiple of a positive real power.
```
lemma eventually_log_pow_lt_mul_rpow (n : ℕ) (r c : ℝ) (hr : 0 < r) (hc : 0 < c) :
    ∀ᶠ x : ℝ in atTop, (Real.log x) ^ n < c * x ^ r := by
…
```
lemma OAI.Problem337.eventually_exceptional_triples_lt_main_term line 24
Source documentation
The exceptional-prime triple estimate is lower order than the quantitative three-prime main term. This is purely an asymptotic comparison, not a three-prime theorem.
```
lemma eventually_exceptional_triples_lt_main_term (C c : ℝ) (hC : 0 ≤ C) (hc : 0 < c) :
    ∀ᶠ x : ℝ in atTop,
      C * x ^ (7 / 4 : ℝ) * Real.log x * Real.log (Real.log x) <
        c * x ^ (2 : ℕ) / (Real.log x) ^ 3 := by
…
```

lemma OAI.Problem337.eventually_exceptional_prime_triple_count_small line 55

Source documentation

Natural-index form targeting a count of exceptional primes: the elementary bound 3 * u * B u for contaminated ordered triples is negligible.

lemma eventually_exceptional_prime_triple_count_small (B : ℕ → ℕ) (C c : ℝ)
    (hC : 0 ≤ C) (hc : 0 < c)
    (hB : ∀ᶠ u : ℕ in atTop,
      (B u : ℝ) ≤ C * (u : ℝ) ^ (3 / 4 : ℝ) * Real.log (u : ℝ) *
        Real.log (Real.log (u : ℝ))) :
    ∀ᶠ u : ℕ in atTop,
      (3 : ℝ) * (u : ℝ) * (B u : ℝ) <
        c * (u : ℝ) ^ (2 : ℕ) / Real.log (u : ℝ) ^ 3 := by
…