mFourierBasis — Mathlib

English

mFourierBasis is the Hilbert basis for L²(UnitAddTorus d) indexed by integer d-vectors.

Русский

mFourierBasis есть хилбертовский базис для L²(UnitAddTorus d), индексируемый целочисленными векторами.

LaTeX

$$$$\\text{mFourierBasis} : \\text{HilbertBasis} (d \\to \\mathbb{Z}) \\mathbb{C} \\ L^2(UnitAddTorus d).$$$$

Lean4

/-- We define `mFourierBasis` to be a `ℤᵈ`-indexed Hilbert basis for the `L²` space of functions
on `UnitAddTorus d`, which by definition is an isometric isomorphism from `L²(UnitAddTorus d)`
to `ℓ²(ℤᵈ, ℂ)`. -/
def mFourierBasis : HilbertBasis (d → ℤ) ℂ L²(UnitAddTorus d) :=
  HilbertBasis.mk orthonormal_mFourier (span_mFourierLp_closure_eq_top (by simp)).ge

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