IsUpperMoebius — Mathlib

English

A sequence muPlus is called upper Moebius if for every n, the sum over divisors of n of muPlus(d) dominates the unit at n (which is 1 if n=1 and 0 otherwise).

Русский

Последовательность muPlus называется верхней мёбиусовой, если для каждого n сумма по делителям n muPlus(d) не меньше δ_{n,1}.

LaTeX

$$IsUpperMoebius(muPlus) := ∀ n, (if n = 1 then 1 else 0) ≤ ∑_{d ∣ n} muPlus(d)$$

Lean4

/-- A sequence of coefficients $\mu^{+}$ is upper Moebius if $\mu * \zeta ≤ \mu^{+} * \zeta$. These
  coefficients then yield an upper bound on the sifted sum. -/
def IsUpperMoebius (muPlus : ℕ → ℝ) : Prop :=
  ∀ n : ℕ, (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d

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