The sifted von Mangoldt weight is nonnegative
ProvedTaoFivePrimes.siftedVonMangoldt_nonnegcircle-methodnumber-theoryprime-numbers
The sifted von Mangoldt weight , which removes from every sharing a prime factor with the primorial of , is nonnegative for all and . It is either , which is nonnegative, or zero.
This is the weight appearing in equation (8.10) and, with the modulus , in the exponential sums that Theorem 1.3 estimates.
Preamble
import Mathlib import Definitions.Def_TaoFivePrimes_RepresentationCount open TaoFivePrimes
Formal statement
namespace TaoFivePrimes theorem siftedVonMangoldt_nonneg (N n : ℕ) : 0 ≤ siftedVonMangoldt N n := by sorry end TaoFivePrimes
Source
Terence Tao, Every odd number greater than 1 is the sum of at most five primes, Mathematics of Computation 83 (2014), 997-1038, https://arxiv.org/abs/1201.6656, Section 8, equation (8.10); nonnegativity of the von Mangoldt function is standard.