The sum over prime arguments in a real interval #
noncomputable def
NairTenenbaum.primeShortSum
{k : ℕ}
(Q : Fin k → Polynomial ℤ)
(F : ArithmeticMap k)
(x y : ℝ)
:
The left side of Theorem 3.
Equations
- NairTenenbaum.primeShortSum Q F x y = ∑ p ∈ NairTenenbaum.shortInterval x y with Nat.Prime p, NairTenenbaum.extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval (↑p) (Q j)).natAbs
Instances For
theorem
NairTenenbaum.PolynomialSystem.primeShortSum_eq_primeIntegerSum
{k r : ℕ}
(P : PolynomialSystem k r)
(F : ArithmeticMap k)
{x : ℝ}
(hx : 0 ≤ x)
(y : ℝ)
: