Theorems · Theorem · harmonic analysis

fourierCoeff_eq_intervalIntegral

∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  (f : AddCircle T → E) (n : ℤ) (a : ℝ), fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f ↑x

The Fourier coefficients of a function on AddCircle T can be computed as an integral over [a, a + T], for any real a.

Defined in

Mathlib.Analysis.Fourier.AddCircle

Cited by

4 results in Mathlib

Foundations

Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FactNormedAddCommGroupNormedSpace