smoothingFn — Mathlib

English

The smoothing function ε(n) is little-o of the constant 1 function, i.e., ε = o[atTop] 1.

Русский

Сглаживающая функция ε(n) есть малый порядок по отношению к константе 1: ε = o[atTop] 1.

LaTeX

$$$\varepsilon(n) = o(1) \quad (n\to\infty)$$$

Lean4

/-- The "smoothing function" is defined as `1 / log n`. This is defined as an `ℝ → ℝ` function
as opposed to `ℕ → ℝ` since this is more convenient for the proof, where we need to e.g. take
derivatives. -/
noncomputable def smoothingFn (n : ℝ) : ℝ :=
  1 / log n

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