SieveScale.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic truncation length is negligible compared with the physical interval exponent in the finite rough sieve.

theorem OAI.TwoPointCorrelations.eventually_sieve_boundary_exponent line 15
Source documentation
Any fixed exp(O(L^.99 log L)) counting cost is absorbed by the interval length exp(L^.995), with the explicit power needed below.
Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveScale.lean:15 (same declaration text).
```
theorem eventually_sieve_boundary_exponent (K : ℝ) (hK : 0 ≤ K) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (K * L ^ (99 / 100 : ℝ) * Real.log L - L ^ (199 / 200 : ℝ)) ≤
        L ^ (-100 : ℝ) := by
…
```