English
If muPlus is an upper Moebius function, then s.siftedSum ≤ s.totalMass · mainSum(muPlus) + errSum(muPlus).
Русский
Если muPlus — верхняя Моебиусова функция, то s.siftedSum ≤ s.totalMass · mainSum(muPlus) + errSum(muPlus).
LaTeX
$$s.siftedSum ≤ s.totalMass * mainSum(muPlus) + errSum(muPlus)$$
Lean4
theorem siftedSum_le_mainSum_errSum_of_upperMoebius (muPlus : ℕ → ℝ) (h : IsUpperMoebius muPlus) :
s.siftedSum ≤ s.totalMass * s.mainSum muPlus + s.errSum muPlus :=
calc
s.siftedSum ≤ ∑ d ∈ divisors s.prodPrimes, muPlus d * multSum d := siftedSum_le_sum_of_upperMoebius _ h
_ = s.totalMass * mainSum muPlus + ∑ d ∈ divisors s.prodPrimes, muPlus d * s.rem d :=
by
rw [mainSum, mul_sum, ← sum_add_distrib]
congr with d
dsimp only [rem]; ring
_ ≤ s.totalMass * mainSum muPlus + errSum muPlus := by
rw [errSum]
gcongr _ + ∑ d ∈ _, ?_ with d
rw [← abs_mul]
exact le_abs_self (muPlus d * s.rem d)
