coeFn_fourierLp — Mathlib

English

The a.e. equality between the fourierLp p n and the function f_n holds: the Lp representative of fourierLp p n is ae-equal to f_n.

Русский

С равенством почти по мере: эквивалентность ae между fourierLp p n и f_n.

LaTeX

$$fourierLp p n =ᵐ[haarAddCircle] fourier n$$

Lean4

theorem coeFn_fourierLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (n : ℤ) : @fourierLp T hT p _ n =ᵐ[haarAddCircle] fourier n :=
  coeFn_toLp haarAddCircle (fourier n)

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