English
The n-th Fourier coefficient of a function f: AddCircle(T) → E (E a complete normed space) can be computed as the integral over any interval of length T: ∫_{a}^{a+T} f̃(x) dx with the appropriate weighting by fourier (−n).
Русский
n-й коэффициент Фурье функции f: AddCircle(T) → E может быть вычислен как интеграл по произвольному интервалу длины T.
LaTeX
$$fourierCoeff f n = (1/T) ∙ ∫_{a}^{a+T} fourier (−n) x • f x dx$$
Lean4
/-- The Fourier coefficients of a function on `AddCircle T` can be computed as an integral
over `[a, a + T]`, for any real `a`. -/
theorem fourierCoeff_eq_intervalIntegral (f : AddCircle T → E) (n : ℤ) (a : ℝ) :
fourierCoeff f n = (1 / T) • ∫ x in a..a + T, @fourier T (-n) x • f x :=
by
have : ∀ x : ℝ, @fourier T (-n) x • f x = (fun z : AddCircle T => @fourier T (-n) z • f z) x := by intro x;
rfl
-- After https://github.com/leanprover/lean4/pull/3124, we need to add `singlePass := true` to avoid an infinite loop.
simp_rw +singlePass [this]
rw [fourierCoeff, AddCircle.intervalIntegral_preimage T a (fun z => _ • _), volume_eq_smul_haarAddCircle,
integral_smul_measure, ENNReal.toReal_ofReal hT.out.le, ← smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne',
one_smul]
