English
For each p with 1 ≤ p, the family fourier n defines elements of Lp(ℂ, p) on AddCircle(T); the function fourier n considered as an Lp function coincides a.e. with the pointwise monomial.
Русский
Для каждого p с 1 ≤ p мономии fourier n образуют элементы Lp(ℂ, p) на AddCircle(T); функция fourier n как элемент Lp равна почти повсеместно самой мономиале.
LaTeX
$$fourier n ∈ Lp(ℂ, p) (AddCircle.haarAddCircle)$$
Lean4
/-- The family of monomials `fourier n`, parametrized by `n : ℤ` and considered as
elements of the `Lp` space of functions `AddCircle T → ℂ`. -/
abbrev fourierLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (n : ℤ) : Lp ℂ p (@haarAddCircle T hT) :=
toLp (E := ℂ) p haarAddCircle ℂ (fourier n)
