SupplyAsymptotics.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.supply_log_factor_isLittleO line 12
Source documentation
The logarithms lost in the exceptional-prime count are absorbed by any positive power of the main parameter.
```
theorem supply_log_factor_isLittleO (δ : ℝ) (hδ : 0 < δ) :
    (fun x : ℝ => Real.log x ^ 4 * Real.log (Real.log x)) =o[atTop]
      (fun x : ℝ => x ^ δ) := by
…
```
theorem OAI.Problem337.supply_exceptional_triples_isLittleO line 35
Source documentation
Exceptional prime triples in the rational-divisor supply have lower order than the quantitative three-prime main term. This is only the analytic comparison; no three-prime theorem is assumed or asserted here.
```
theorem supply_exceptional_triples_isLittleO :
    (fun x : ℝ => x ^ (7 / 4 : ℝ) * Real.log x * Real.log (Real.log x))
      =o[atTop] (fun x : ℝ => x ^ 2 / Real.log x ^ 3) := by
…
```

theorem OAI.Problem337.supply_exceptional_triples_eventually_lt line 51

Source documentation

Any fixed multiple of the exceptional count is eventually smaller than any positive fixed multiple of the main term.

theorem supply_exceptional_triples_eventually_lt (C 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
…

theorem OAI.Problem337.supply_bad_triples_eventually_lt line 67

Source documentation

Direct natural-parameter form of the estimate used to discard triples containing one of the exceptional primes.

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