rem — Mathlib

English

The remainder term is the difference between the total weight of multiples of d and the main term ν(d) times total mass.

Русский

Остаток — разница между суммарным весом кратных d и главным членом ν(d) умноженным на общую массу.

LaTeX

$$rem(d) = multSum(d) - nu(d) * totalMass$$

Lean4

/-- The remainder term in the approximation A_d = ν (d) X + R_d. This is the degree to which `nu`
  fails to approximate the proportion of the weight that is a multiple of `d`. -/
@[simp]
def rem (d : ℕ) : ℝ :=
  s.multSum d - s.nu d * s.totalMass

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