The literal prime-progression density in the omega(d)/d convention

The inverse totient is retained on prime powers. No squarefree extension is substituted in either the full-modulus remainder or the density numerator.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.densityNumerator (g : ArithmeticFunction ℝ) : ArithmeticFunction ℝ

Equations

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

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.densityNumerator_isMultiplicative {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) : (densityNumerator g).IsMultiplicative

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeDensity_densityNumerator (g : ArithmeticFunction ℝ) : SmallRosser.primeDensity (densityNumerator g) = g

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.progressionDensity_isMultiplicative (a : ℕ) : (progressionDensity a).IsMultiplicative

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