UpperSieveInput.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Published finite-event upper sieve

Theorem 2.4 of Kevin Ford, Sieve Methods Lecture Notes, Spring 2023, page 18, https://ford126.web.illinois.edu/sieve2023.pdf, in its general probability-space formulation (Section 1.2). The sum of absolute remainders is only over squarefree products at most the sifting bound. No arithmetic progression estimate or application-specific weight bound is assumed here.

def OAI.JointDickman.sieveIntersection line 21

Source documentation

Mass of the intersection of the events indexed by D.

noncomputable def sieveIntersection {X : Type*} [Fintype X]
    (E : X → Finset ℕ) (w : X → ℝ) (D : Finset ℕ) : ℝ :=
…

def OAI.JointDickman.sieveRemainder line 26

Source documentation

Ford's remainder r_d, with D the prime factors of d.

noncomputable def sieveRemainder {X : Type*} [Fintype X]
    (E : X → Finset ℕ) (w : X → ℝ) (M : ℝ) (g : ℕ → ℝ)
    (D : Finset ℕ) : ℝ := sieveIntersection E w D - M * ∏ p ∈ D, g p

Mentions: OAI.JointDickman.sieveIntersection

def OAI.JointDickman.SieveDimension line 31
Source documentation
Ford's interval condition (Ω). Primes outside P have local density zero.
```
def SieveDimension (P : Finset ℕ) (g : ℕ → ℝ) (κ A z : ℝ) : Prop :=
…
```
def OAI.JointDickman.PublishedInputs.FordUpperSieveInput line 42
Source documentation
Ford 2023, Theorem 2.4, specialized to a finite nonnegative population. The constant is independent of the population, events, densities and bound. The parameter M is the main-term mass X in the source; its difference from the actual population mass is retained in the D = ∅ remainder.
```
def FordUpperSieveInput : Prop :=
…
```

theorem OAI.JointDickman.SieveDimension.mono line 58

Source documentation

Decreasing the local densities preserves Ford's dimension condition.

theorem SieveDimension.mono {P : Finset ℕ} {g h : ℕ → ℝ} {κ A z : ℝ}
    (hd : SieveDimension P g κ A z)
    (hgh : ∀ p ∈ P, h p ≤ g p) (hg : ∀ p ∈ P, g p < 1) :
    SieveDimension P h κ A z := by
…

Mentions: OAI.JointDickman.SieveDimension

theorem OAI.JointDickman.SieveDimension.subset line 73

Source documentation

Deleting sieve primes also preserves the dimension condition.

theorem SieveDimension.subset {P S : Finset ℕ} {g : ℕ → ℝ} {κ A z : ℝ}
    (hd : SieveDimension P g κ A z) (hS : S ⊆ P)
    (hg : ∀ p ∈ P, 0 ≤ g p ∧ g p < 1) :
    SieveDimension S g κ A z := by
…

Mentions: OAI.JointDickman.SieveDimension