SieveProducts.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Local-density products for the rough sieve. The only prime information needed for the product estimate is a lower bound for the ordinary reciprocal sum.

lemma OAI.TwoPointCorrelations.reciprocal_square_sum_le_one line 14
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveProducts.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.one_sub_product_le_exp line 29
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveProducts.lean:29 (same declaration text).
theorem OAI.TwoPointCorrelations.fourForm_product_bound line 45
Source documentation
Four-form local avoidance loses precisely four reciprocal prime sums, up to an absolute constant from the convergent square sum.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveProducts.lean:45 (same declaration text).
```
theorem fourForm_product_bound (P : Finset ℕ) [∀ p : P, NeZero (p : ℕ)]
    (hP : ∀ p ∈ P, 2 ≤ p) :
    (∏ p : P, (1 - fourFormBadDensity (p : ℕ))) ≤
      Real.exp 6 * Real.exp (-4 * ∑ p ∈ P, 1 / (p : ℝ)) := by
…
```
Mentions: OAI.TwoPointCorrelations.fourFormBadDensity
theorem OAI.TwoPointCorrelations.oneForm_product_bound line 72
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveProducts.lean:72 (same declaration text).
theorem OAI.TwoPointCorrelations.oneForm_product_scale line 86
Source documentation
The lower half of the classical reciprocal-prime estimate gives the one-form power saving, with its constant displayed.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveProducts.lean:86 (same declaration text).
```
theorem oneForm_product_scale (P : Finset ℕ) (hP : ∀ p ∈ P, 2 ≤ p)
    (L C : ℝ) (hL : 0 < L)
    (hprime : (99 / 100 : ℝ) * Real.log L - C ≤ ∑ p ∈ P, 1 / (p : ℝ)) :
    (∏ p ∈ P, (1 - 1 / (p : ℝ))) ≤ Real.exp C * L ^ (-99 / 100 : ℝ) := by
…
```

theorem OAI.TwoPointCorrelations.fourForm_product_scale line 97

Source documentation

The same classical lower bound gives the full fourth-moment exponent.

Also declared: OAI/NumberTheory/TwoPoint/Bounds/SieveProducts.lean:97 (same declaration text).

theorem fourForm_product_scale (P : Finset ℕ) [∀ p : P, NeZero (p : ℕ)]
    (hP : ∀ p ∈ P, 2 ≤ p) (L C : ℝ) (hL : 0 < L)
    (hprime : (99 / 100 : ℝ) * Real.log L - C ≤ ∑ p ∈ P, 1 / (p : ℝ)) :
    (∏ p : P, (1 - fourFormBadDensity (p : ℕ))) ≤
      Real.exp (4 * C + 6) * L ^ (-99 / 25 : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.fourFormBadDensity