Fourier Series

The purpose of this file is to include some results on Fourier series.

def HasFourierSeries {U : Set ℂ} (f : ↑U → ℂ) (c : ℕ → ℂ) : Prop

Predicate for a function f : U → ℂ to have c : ℕ → ℂ as its fourier series, ie for all x ∈ U, ∑' n, c n * exp (π * I * n * x) = f x. Note we write this using HasSum to assert that the sum exists and is equal to f x.

Equations

• HasFourierSeries f c = ∀ (x : ↑U), HasSum (fun (n : ℕ) => c n * Complex.exp (↑Real.pi * Complex.I * ↑n * ↑x)) (f x)

def Has2PiFourierSeries {U : Set ℂ} (f : ↑U → ℂ) (c : ℕ → ℂ) : Prop

Predicate for a function f : U → ℂ to have c : ℕ → ℂ as its 2π-fourier series, ie for all x ∈ U, ∑' n, c n * exp (2 * π * I * n * x) = f x. Note we write this using HasSum to assert that the sum exists and is equal to f x.

Equations

• Has2PiFourierSeries f c = ∀ (x : ↑U), HasSum (fun (n : ℕ) => c n * Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑x)) (f x)

theorem hasFourierSeries_iff_has2PiFourierSeries {U : Set ℂ} (f : ↑U → ℂ) (c : ℕ → ℂ) : Has2PiFourierSeries f c ↔ HasFourierSeries f (Function.extend (fun (n : ℕ) => 2 * n) c 0)