The weighted second-class exceptional sum

noncomputable def NairTenenbaum.PolynomialSystem.primePowerContribution {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (z : ℝ) (a b : ℤ) : ℝ

The arithmetic contribution of the small-prime power exceptional set.

Equations

• P.primePowerContribution F z a b = ∑ t ∈ NairTenenbaum.primePowerExceptionalSet P.R z (z ^ 3) a b, NairTenenbaum.extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs