Theorems · Definition · harmonic analysis

fourierCoeffOn

{E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → {a b : ℝ} → a < b → (ℝ → E) → ℤ → E

For a function on ℝ, the Fourier coefficients of f on [a, b] are defined as the Fourier coefficients of the unique periodic function agreeing with f on Ioc a b.

Defined in

Mathlib.Analysis.Fourier.AddCircle

Cited by

13 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace