PrimePairSieveModel.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.PrimePairSieve.fiberWeight line 12
Source documentation
Pushing a finite set through a noninjective map retains the multiplicity of each image value. In particular, the two ordered Goldbach pairs with coordinates exchanged must not be identified by the polynomial map.
```
def fiberWeight (A : Finset ℕ) (f : ℕ → ℕ) (y : ℕ) : ℝ :=
…
```
lemma OAI.Problem337.PrimePairSieve.fiberWeight_nonneg line 15
lemma OAI.Problem337.PrimePairSieve.sum_fiberWeight_indicator line 19

def OAI.Problem337.PrimePairSieve.imageSieve line 40

Source documentation

A concrete BoundingSieve attached to any polynomial image, with exact fiber weights rather than an unjustified injectivity assumption.

def imageSieve (A : Finset ℕ) (f : ℕ → ℕ) (P : ℕ)
    (hP : Squarefree P) (ν : ArithmeticFunction ℝ)
    (hν : ν.IsMultiplicative)
    (hνpos : ∀ p : ℕ, p.Prime → p ∣ P → 0 < ν p)
    (hνlt : ∀ p : ℕ, p.Prime → p ∣ P → ν p < 1) : BoundingSieve where
…

lemma OAI.Problem337.PrimePairSieve.imageSieve_multSum line 56
lemma OAI.Problem337.PrimePairSieve.imageSieve_siftedSum line 65
def OAI.Problem337.PrimePairSieve.primePairs line 75
Source documentation
First coordinates of the ordered representations of N by two primes.
```
def primePairs (N : ℕ) : Finset ℕ :=
…
```
def OAI.Problem337.PrimePairSieve.siftedPairs line 79
Source documentation
The original integer coordinates left after sieving both prime factors.
```
def siftedPairs (N P : ℕ) : Finset ℕ :=
…
```
theorem OAI.Problem337.PrimePairSieve.primePairs_subset line 84
Source documentation
A prime pair is either sifted or has a coordinate among the prime divisors of P. This is the exact small-prime correction, valid even for N=0,1.
```
theorem primePairs_subset (N P : ℕ) (hP : P ≠ 0) :
    primePairs N ⊆ siftedPairs N P ∪
      (P.primeFactors ∪ P.primeFactors.image (fun p => N - p)) := by
…
```
Mentions: OAI.Problem337.PrimePairSieve.primePairs, OAI.Problem337.PrimePairSieve.siftedPairs
theorem OAI.Problem337.PrimePairSieve.card_primePairs_le_sifted line 108
Source documentation
At most twice the number of sieving primes is lost when passing from ordered prime pairs to sifted polynomial values with multiplicities.
```
theorem card_primePairs_le_sifted (N P : ℕ) (hP : P ≠ 0) :
    (primePairs N).card ≤ (siftedPairs N P).card + 2 * P.primeFactors.card := by
…
```
Mentions: OAI.Problem337.PrimePairSieve.primePairs, OAI.Problem337.PrimePairSieve.siftedPairs

lemma OAI.Problem337.PrimePairSieve.imageSieve_rem line 126

Source documentation

The exact polynomial divisor count is the remainder term supplied to the Selberg sieve; no analytic approximation is built into this model.

lemma imageSieve_rem (A : Finset ℕ) (f : ℕ → ℕ) (P : ℕ)
    (hP : Squarefree P) (ν : ArithmeticFunction ℝ)
    (hν : ν.IsMultiplicative)
    (hνpos : ∀ p : ℕ, p.Prime → p ∣ P → 0 < ν p)
    (hνlt : ∀ p : ℕ, p.Prime → p ∣ P → ν p < 1) (d : ℕ) :
    (imageSieve A f P hP ν hν hνpos hνlt).rem d =
      ((A.filter (fun x => d ∣ f x)).card : ℝ) - ν d * A.card := by
…

Mentions: OAI.Problem337.PrimePairSieve.imageSieve

theorem OAI.Problem337.PrimePairSieve.primePairs_lambdaSquared_bound line 139

Source documentation

A fully concrete prime-pair Λ² bound with ordered-pair multiplicities and an explicit small-prime correction. The main coefficient and its arithmetic remainder are still to be estimated by the sieve application.

theorem primePairs_lambdaSquared_bound (N P : ℕ)
    (hP : Squarefree P) (ν : ArithmeticFunction ℝ)
    (hν : ν.IsMultiplicative)
    (hνpos : ∀ p : ℕ, p.Prime → p ∣ P → 0 < ν p)
    (hνlt : ∀ p : ℕ, p.Prime → p ∣ P → ν p < 1)
    (w : ℕ → ℝ) (hw : w 1 = 1) :
    ((primePairs N).card : ℝ) ≤
      ((Finset.Icc 1 (N - 1)).card : ℝ) *
        (∑ d ∈ P.divisors, BoundingSieve.lambdaSquared w d * ν d) +
      (∑ d ∈ P.divisors, |BoundingSieve.lambdaSquared w d| *
        |(((Finset.Icc 1 (N - 1)).filter
            (fun x => d ∣ x * (N - x))).card : ℝ) -
…

Mentions: OAI.Problem337.PrimePairSieve.primePairs