English
If muPlus is an upper Moebius function, then s.siftedSum is bounded by the Dirichlet-type sum over divisors of s.prodPrimes, μ⁺(d) · multSum(d).
Русский
Если muPlus — верхняя Моебиусова функция, то s.siftedSum ограничено по сумме по делителям s.prodPrimes: μ⁺(d) · multSum(d).
LaTeX
$$s.siftedSum ≤ ∑_{d ∣ s.prodPrimes} muPlus(d) · multSum(d)$$
Lean4
theorem siftedSum_le_sum_of_upperMoebius (muPlus : ℕ → ℝ) (h : IsUpperMoebius muPlus) :
s.siftedSum ≤ ∑ d ∈ divisors s.prodPrimes, muPlus d * s.multSum d :=
by
have hμ : ∀ n, (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d := h
calc
siftedSum ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (Nat.gcd s.prodPrimes n).divisors, muPlus d := ?caseA
_ = ∑ n ∈ s.support, ∑ d ∈ divisors s.prodPrimes, if d ∣ n then s.weights n * muPlus d else 0 := ?caseB
_ = ∑ d ∈ divisors s.prodPrimes, muPlus d * multSum d := ?caseC
case caseA =>
rw [siftedSum_eq_sum_support_mul_ite]
gcongr with n
exact hμ (Nat.gcd s.prodPrimes n)
case caseB =>
simp_rw [mul_sum, ← sum_filter]
congr with n
congr
· rw [← divisors_filter_dvd_of_dvd prodPrimes_ne_zero (Nat.gcd_dvd_left _ _)]
ext x; simp +contextual [dvd_gcd_iff]
case caseC =>
rw [sum_comm]
simp_rw [multSum, ← sum_filter, mul_sum, mul_comm]
