F_nat — Mathlib

English

F_nat(k, a, t) is the sum over all n ∈ ℕ of f_nat(k, a, t, n). It represents the total bound for the ℕ-version of the Hurwitz kernel sum.

Русский

F_nat(k, a, t) есть сумма по всем n ∈ ℕ от f_nat(k, a, t, n); выражает общую границу для частичной суммы Хурвица.

LaTeX

$$$F_{nat}(k,a,t) = \sum_{n=0}^{\infty} f_{nat}(k,a,t,n).$$$

Lean4

/-- The sum to be bounded (`ℕ` version). -/
def F_nat (k : ℕ) (a t : ℝ) : ℝ :=
  ∑' n, f_nat k a t n

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