logMul — Mathlib

English

The pointwise product of the logarithm with a sequence f is defined by (logMul f)(n) = log(n) · f(n).

Русский

Покажем точечное произведение логарифма и последовательности f: (logMul f)(n) = log(n) · f(n).

LaTeX

$$$\logMul f = (n \mapsto \log n \cdot f(n))$$$

Lean4

/-- The (point-wise) product of `log : ℕ → ℂ` with `f`. -/
noncomputable abbrev logMul (f : ℕ → ℂ) (n : ℕ) : ℂ :=
  log n * f n

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