Fourier analysis of uniformly almost periodic functions

noncomputable def mean (f : ℝ → ℂ) : ℂ

The mean of an uniformly almost periodic function f is the limit of its average on [0, X] as X → +∞.

Equations

• mean f = Filter.atTop.limUnder fun (X : ℝ) => ⨍ (x : ℝ) in 0..X, f x

theorem IsUnifAlmostPeriodic.tendsto_mean {f : ℝ → ℂ} (hf : IsUnifAlmostPeriodic f) : Filter.Tendsto (fun (X : ℝ) => ⨍ (x : ℝ) in 0..X, f x) Filter.atTop (nhds (mean f))

noncomputable def meanFourierCoeff (Λ : ℝ) (f : ℝ → ℂ) : ℂ

The Fourier coefficient at Λ of an uniformly almost periodic function f is the mean of x ↦ f x * exp (-iΛx).

Equations

• meanFourierCoeff Λ f = mean fun (x : ℝ) => f x * Complex.exp (-Complex.I * ↑Λ * ↑x)

theorem IsUnifAlmostPeriodic.countable_meanFourierCoeff_ne_zero {f : ℝ → ℂ} : {Λ : ℝ | meanFourierCoeff Λ f ≠ 0}.Countable

The Fourier exponents of an uniformly almost periodic function f are at most countable.