f_nat — Mathlib

English

The summand used in the ℕ-version is defined by f_nat(k, a, t, n) = (n + a)^k · exp(-π (n + a)^2 t).

Русский

Слагаемая в числовой версии определяется как f_nat(k, a, t, n) = (n + a)^k · e^{-π (n + a)^2 t}.

LaTeX

$$$f_{nat}(k, a, t, n) = (n + a)^k \cdot e^{-\pi (n + a)^2 t}.$$$

Lean4

/-- Summand in the sum to be bounded (`ℕ` version). -/
def f_nat (k : ℕ) (a t : ℝ) (n : ℕ) : ℝ :=
  (n + a) ^ k * exp (-π * (n + a) ^ 2 * t)

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