The actual progression density, in the standard multiplicative omega interface. All identities retain the given density at every natural number, including zero.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.progressionOmega (v : ℕ) : ArithmeticFunction ℝ

The actual sieve weight, not a squarefree surrogate.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.progressionOmega v = { toFun := fun (n : ℕ) => ↑n * (MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity v) n, map_zero' := ⋯ }

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.progressionOmega_apply (v n : ℕ) : (progressionOmega v) n = ↑n * (progressionDensity v) n

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.progressionOmega_isMultiplicative (v : ℕ) : (progressionOmega v).IsMultiplicative

Multiplicativity is proved directly from coprimality and Euler's totient.

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeDensity_progressionOmega_apply (v n : ℕ) : (SmallRosser.primeDensity (progressionOmega v)) n = (progressionDensity v) n

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeDensity_progressionOmega (v : ℕ) : SmallRosser.primeDensity (progressionOmega v) = progressionDensity v

Equality as arithmetic functions, with no nonzero or squarefree restriction.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity_prime (v : ℕ) {p : ℕ} (hp : Nat.Prime p) : (progressionDensity v) p = if p.Coprime v then 1 / (↑p - 1) else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity_prime_nonneg_lt_one (v : ℕ) {p : ℕ} (hp : Nat.Prime p) (hp2 : 2 < p) : 0 ≤ (progressionDensity v) p ∧ (progressionDensity v) p < 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.progressionOmega_prime_nonneg_lt_one (v : ℕ) {p : ℕ} (hp : Nat.Prime p) (hp2 : 2 < p) : 0 ≤ (progressionOmega v) p / ↑p ∧ (progressionOmega v) p / ↑p < 1

Prime hypotheses in exactly the quotient form expected by ExternalSieve.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.progressionOmega_eulerProduct (v : ℕ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) : ∏ p ∈ P, (1 - (progressionOmega v) p / ↑p) = ∏ p ∈ P, (1 - if p.Coprime v then 1 / (↑p - 1) else 0)

The genuine Euler product, on any finite set of primes.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.progressionOmega_eulerProduct_filter (v : ℕ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) : ∏ p ∈ P, (1 - (progressionOmega v) p / ↑p) = ∏ p ∈ P with p.Coprime v, (1 - 1 / (↑p - 1))

Primes dividing the progression parameter contribute the exact unit factor.