Concrete prime intervals and the exact support of the independent sieve loss.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta (n : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta n = if Nat.Prime n then 1 else 0

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval (u v : ℝ) : Finset ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval u v = Finset.Ioc ⌊u⌋₊ ⌊v⌋₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_deleted_subset (N : Finset ℕ) {h : ℕ} (hh : h ≠ 0) : {n ∈ N | Nat.Prime n ∧ ¬n.Coprime h} ⊆ h.primeFactors

The independent sieve deletes only prime divisors of its own modulus.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_deleted_card_le (N : Finset ℕ) {h : ℕ} (hh : h ≠ 0) : {n ∈ N | Nat.Prime n ∧ ¬n.Coprime h}.card ≤ h.primeFactors.card

The loss count is uniform in the interval and in the progression.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta_nonneg (n : ℕ) : 0 ≤ primeSWBeta n

The literal prime coefficient, without an additional coprimality mask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_primeFactors_le_tau (h : ℕ) : h.primeFactors.card ≤ (fouvryTau 2) h

The loss is absorbed by the fixed second divisor function.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWSum (N : Finset ℕ) (P : ℕ → Prop) [DecidablePred P] : ℝ

Prime mass subject to a literal predicate.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWSum N P = ∑ n ∈ N, if P n then MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta n else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWSum_eq_card (N : Finset ℕ) (P : ℕ → Prop) [DecidablePred P] : primeSWSum N P = ↑{n ∈ N | Nat.Prime n ∧ P n}.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWSum_nonneg (N : Finset ℕ) (P : ℕ → Prop) [DecidablePred P] : 0 ≤ primeSWSum N P

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWSum_sieve_sub (N : Finset ℕ) (P : ℕ → Prop) [DecidablePred P] (h : ℕ) : (primeSWSum N fun (n : ℕ) => P n ∧ n.Coprime h) - primeSWSum N P = -primeSWSum N fun (n : ℕ) => P n ∧ ¬n.Coprime h

Exact deletion identity; the same predicate occurs on both sides.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWSum_sieve_abs_sub_le (N : Finset ℕ) (P : ℕ → Prop) [DecidablePred P] {h : ℕ} (hh : h ≠ 0) : |(primeSWSum N fun (n : ℕ) => P n ∧ n.Coprime h) - primeSWSum N P| ≤ ↑((fouvryTau 2) h)

Uniform sieve perturbation for every predicate, not an SW assertion for subsets.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_sieve_discrepancy_sub_le (N : Finset ℕ) {d h : ℕ} (hd : 0 < d) (hh : 0 < h) (b : ℕ) : |betaCoprimeAPDiscrepancy N primeSWBeta d h b - betaCoprimeAPDiscrepancy N primeSWBeta d 1 b| ≤ 2 * ↑((fouvryTau 2) h)

The totient denominator in the centering term is retained explicitly.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_discrepancy_one (N : Finset ℕ) (h b : ℕ) : betaCoprimeAPDiscrepancy N primeSWBeta 1 h b = 0

The modulus-one endpoint vanishes even with the independent sieve.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWSum_mono (N M : Finset ℕ) (P Q : ℕ → Prop) [DecidablePred P] [DecidablePred Q] (hNM : N ⊆ M) (hPQ : ∀ n ∈ N, P n → Q n) : primeSWSum N P ≤ primeSWSum M Q

A predicate can only decrease the literal prime mass.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_discrepancy_eq (N : Finset ℕ) (d h b : ℕ) : betaCoprimeAPDiscrepancy N primeSWBeta d h b = (primeSWSum N fun (n : ℕ) => n.Coprime h ∧ n ≡ b [MOD d]) - (primeSWSum N fun (n : ℕ) => n.Coprime (d * h)) / ↑d.totient

The original discrepancy, expressed with literal prime masses.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWSum_le_card (N : Finset ℕ) (P : ℕ → Prop) [DecidablePred P] : primeSWSum N P ≤ ↑N.card

Absolute mass never exceeds the number of available integers.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_discrepancy_le_card (N : Finset ℕ) {d : ℕ} (hd : 0 < d) (h b : ℕ) : |betaCoprimeAPDiscrepancy N primeSWBeta d h b| ≤ 2 * ↑N.card

A bounded-scale bound, valid also for modulus one and empty intervals.