bernoulliFourierCoeff — Mathlib

English

Bernoulli Fourier coefficients are defined by the Fourier expansion of bernoulliFun on the circle, indexed by k and n (with complex values).

Русский

Бернулли-фурье коэффициенты задаются фурьеровским разложением bernoulliFun на окружности, индексируются k, n и принимают комплексные значения.

LaTeX

$$$$ bernoulliFourierCoeff(k,n). $$$$

Lean4

/-- The `n`-th Fourier coefficient of the `k`-th Bernoulli function on the interval `[0, 1]`. -/
def bernoulliFourierCoeff (k : ℕ) (n : ℤ) : ℂ :=
  fourierCoeffOn zero_lt_one (fun x => bernoulliFun k x) n

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