mFourier — Mathlib

English

Define the multivariate Fourier monomial mFourier for a d-variable torus as the product of one-dimensional Fourier components across coordinates.

Русский

Определяется мультимирный моном Фурье на многомерном торе как произведение одномерных компонент Фурье по координатам.

LaTeX

$$$$ mFourier(n) = \\prod_{i\\in d} \\mathrm{fourier}(n(i))(x_i) $$$$

Lean4

/-- Exponential monomials in `d` variables. -/
def mFourier : C(UnitAddTorus d, ℂ) where
  toFun x := ∏ i : d, fourier (n i) (x i)
  continuous_toFun := continuous_finset_prod _ fun i _ ↦ (fourier (n i)).continuous.comp (continuous_apply i)

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