SieveBoundary.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit accumulation of the finitely many CRT counting errors.

lemma OAI.TwoPointCorrelations.elementarySymmetric_crude line 13
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveBoundary.lean:13 (same declaration text).
lemma OAI.TwoPointCorrelations.truncatedElementary_crude line 32
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveBoundary.lean:32 (same declaration text).
lemma OAI.TwoPointCorrelations.sieveIntersectionError_factor line 49
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveBoundary.lean:49 (same declaration text).
theorem OAI.TwoPointCorrelations.sieveIntersectionError_crude line 58
Source documentation
If an intersection indexed by S has normalized CRT error at most C * (∏ i∈S, a i) / N, the whole finite truncation costs this explicit quantity. In the application a i is the selected prime and C=1 or 3.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveBoundary.lean:58 (same declaration text).
```
theorem sieveIntersectionError_crude {ι : Type*} (P : Finset ι) (a : ι → ℝ)
    (Y C : ℝ) (hY : 0 ≤ Y) (hC : 0 ≤ C)
    (ha : ∀ i ∈ P, 0 ≤ a i ∧ a i ≤ Y) (N R : ℕ) :
    sieveIntersectionError P (fun S => C / N * ∏ i ∈ S, a i) R ≤
      C / N * (R + 1 : ℕ) * ((P.card : ℝ) * Y + 1) ^ R := by
…
```
Mentions: OAI.TwoPointCorrelations.sieveIntersectionError