SieveBoundaryScale.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit accounting for the finite CRT boundary term.

lemma OAI.TwoPointCorrelations.sieve_boundary_numerator line 11
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveBoundaryScale.lean:11 (same declaration text).
lemma OAI.TwoPointCorrelations.sieve_base_le_exp line 36
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveBoundaryScale.lean:36 (same declaration text).

theorem OAI.TwoPointCorrelations.eventually_sieve_boundary_cost line 51

Source documentation

Uniformly in the modulus cutoff, number of moduli and logarithmic truncation order, the literal finite boundary term is O(L^-100).

Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveBoundaryScale.lean:51 (same declaration text).

theorem eventually_sieve_boundary_cost (C C₀ : ℝ) (hC : 0 ≤ C) (hC₀ : 0 ≤ C₀) :
    ∀ᶠ L : ℝ in atTop, ∀ (Y n : ℝ) (N R : ℕ),
      0 ≤ Y → 0 ≤ n → n ≤ Y → Y ≤ Real.exp (L ^ (99 / 100 : ℝ)) →
      (R : ℝ) ≤ C * Real.log L →
      (1 / 2 : ℝ) * Real.exp (L ^ (199 / 200 : ℝ)) ≤ N →
      C₀ / (N : ℝ) * (R + 1 : ℕ) * (n * Y + 1) ^ R ≤ L ^ (-100 : ℝ) := by
…