mainSum — Mathlib

English

For a weight function muPlus, the main sum is the Dirichlet-type sum over divisors of s.prodPrimes of muPlus(d) times ν(d).

Русский

Для функции весов muPlus главная сумма — это сумма по делителям prodPrimes, muPlus(d) · ν(d).

LaTeX

$$mainSum(muPlus) = ∑_{d ∈ divisors(s.prodPrimes)} muPlus(d) * s.nu(d)$$

Lean4

/-- `X * mainSum μ⁺` is the main term in the upper bound on `sifted_sum`. -/
def mainSum (muPlus : ℕ → ℝ) : ℝ :=
  ∑ d ∈ divisors s.prodPrimes, muPlus d * s.nu d

Похожие утверждения