errSum

Mathlib.NumberTheory.SelbergSieve

URI: https://scilib.ai/kg/mathlib#BoundingSieve.errSum

← MathLib Explorer

English

The error sum is the sum over divisors of the absolute values |muPlus(d)| times |rem(d)|.

Русский

Сумма ошибок — сумма по делителям |muPlus(d)| · |rem(d)|.

LaTeX

$$errSum(muPlus) = \\sum_{d ∣ s.prodPrimes} |muPlus(d)| · |s.rem(d)|$$

Lean4

/-- `errSum μ⁺` is the error term in the upper bound on `sifted_sum`. -/
def errSum (muPlus : ℕ → ℝ) : ℝ :=
  ∑ d ∈ divisors s.prodPrimes, |muPlus d| * |s.rem d|

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru