noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.g9BaseEuler (P : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.g9BaseEuler P = ∏ p ∈ P, (1 - 1 / (↑p - 1))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9_euler_factor_payment {x L : ℝ} (hL : 4 ≤ L) (hx : L ≤ x) : 1 ≤ (1 - 1 / (x - 1)) * (1 + 1 / (L - 2))

Uniform payment for deleting one large prime Euler factor.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9_baseEuler_nonneg (P : Finset ℕ) (hP : ∀ p ∈ P, 2 < p) : 0 ≤ g9BaseEuler P

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9_baseEuler_erase_le (P : Finset ℕ) (hP : ∀ p ∈ P, 2 < p) (q : ℕ) {L : ℝ} (hL : 4 ≤ L) (hq : L ≤ ↑q) : g9BaseEuler (P.erase q) ≤ g9BaseEuler P * (1 + 1 / (L - 2))

Erasing a label costs at most one payment, even when it was already absent.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9_euler_three_primes_exact (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {n s t : ℕ} (hn : Nat.Prime n) (hs : Nat.Prime s) (ht : Nat.Prime t) : ∏ p ∈ P, (1 - (progressionDensity (n * (s * t))) p) = g9BaseEuler (((P.erase n).erase s).erase t)

Exact deletion formula: repeated prime labels require no distinctness.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9_euler_three_primes_le (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ 2 < p) {n s t : ℕ} (hn : Nat.Prime n) (hs : Nat.Prime s) (ht : Nat.Prime t) {L : ℝ} (hL : 4 ≤ L) (hnL : L ≤ ↑n) (hsL : L ≤ ↑s) (htL : L ≤ ↑t) : ∏ p ∈ P, (1 - (progressionDensity (n * (s * t))) p) ≤ g9BaseEuler P * (1 + 1 / (L - 2)) ^ 3

The genuine Euler correction is bounded by three uniform payments. No assumption that the three prime labels are distinct or belong to P.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9_weighted_euler_three_primes_le (P U V : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ 2 < p) (α β : ℕ → ℝ) (hα0 : ∀ m ∈ U, 0 ≤ α m) (hβ0 : ∀ n ∈ V, 0 ≤ β n) {L : ℝ} (hL : 4 ≤ L) (hα : ∀ m ∈ U, α m ≠ 0 → ∃ (s : ℕ) (t : ℕ), Nat.Prime s ∧ Nat.Prime t ∧ m = s * t ∧ L ≤ ↑s ∧ L ≤ ↑t) (hβ : ∀ n ∈ V, β n ≠ 0 → Nat.Prime n ∧ L ≤ ↑n) : ∑ m ∈ U, ∑ n ∈ V, α m * β n * ∏ p ∈ P, (1 - (progressionDensity (m * n)) p) ≤ g9BaseEuler P * (1 + 1 / (L - 2)) ^ 3 * ∑ m ∈ U, ∑ n ∈ V, α m * β n

Finite weighted transfer using only structural prime support. Zero coefficient terms are removed before the prime-label bound is invoked.