mFourierCoeff_toLp — Mathlib

English

The Fourier coefficient computed via the Lp representation matches the original Fourier coefficient.

Русский

Коэффициент Фурье, полученный через представление Lp, совпадает с исходным коэффициентом Фурье.

LaTeX

$$$$ mFourierCoeff\\big(f.toLp(2, volume, \\mathbb{C})\\big)(n) = mFourierCoeff(f)(n). $$$$

Lean4

theorem mFourierCoeff_toLp (n : d → ℤ) : mFourierCoeff (f.toLp 2 volume ℂ) n = mFourierCoeff f n :=
  integral_congr_ae (ae_eq_rfl.mul <| f.coeFn_toAEEqFun _)

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