Fourier coefficients on an interval

Mathlib's fourierCoeffOn hab f n is the n-th Fourier coefficient of f on [a, b], that is, of the (b - a)-periodic function agreeing with f on (a, b]. This file records that the integrand of such a coefficient stays interval-integrable (IntervalIntegrable.fourier_smul), the additivity of fourierCoeffOn on interval-integrable functions (TauCeti.fourierCoeffOn_add, TauCeti.fourierCoeffOn_sub), the interval counterparts of Mathlib's fourierCoeff.add, bounds the coefficients by a sup bound on (a, b] (TauCeti.norm_fourierCoeffOn_le), and computes the coefficients of the Fourier monomials themselves (TauCeti.fourierCoeffOn_fourier), the interval counterpart of Mathlib's fourierCoeff_fourier, in particular for a circle c + w e^{2πimt/(b-a)} (TauCeti.fourierCoeffOn_const_add_mul_fourier). Conversely, a function continuous on [a, b] is determined there by its Fourier coefficients (TauCeti.eqOn_Icc_of_fourierCoeffOn_eq); the endpoint a, which the coefficients do not see, is recovered by continuity. In particular, it is a circle c + w e^{2πist/(b-a)} on [a, b] exactly when its coefficients vanish outside the frequencies 0 and s (TauCeti.exists_eqOn_const_add_mul_fourier_iff).

For a function on AddCircle T, the Fourier coefficients are those of its lift on any period interval (TauCeti.fourierCoeff_eq_fourierCoeffOn). On such an interval, each derivative of a C^k periodic function multiplies its coefficients by 2πin / T (TauCeti.fourierCoeffOn_iteratedDeriv), since periodicity kills the boundary term of the integration by parts. The same holds for a function on the circle with values in any complete normed complex space and a continuous derivative (TauCeti.fourierCoeff_of_hasDerivAt).

theorem IntervalIntegrable.fourier_smul {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} (hf : IntervalIntegrable f MeasureTheory.volume a b) (T : ℝ) (n : ℤ) : IntervalIntegrable (fun (t : ℝ) => (fourier n) ↑t • f t) MeasureTheory.volume a b

Multiplying an interval-integrable function by a Fourier monomial t ↦ fourier n t of any period T keeps it interval-integrable; with T = b - a and frequency -n this is the integrand of fourierCoeffOn_eq_integral.

theorem TauCeti.fourierCoeffOn_add {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hab : a < b) {f g : ℝ → E} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hg : IntervalIntegrable g MeasureTheory.volume a b) (n : ℤ) : fourierCoeffOn hab (fun (t : ℝ) => f t + g t) n = fourierCoeffOn hab f n + fourierCoeffOn hab g n

Fourier coefficients on an interval are additive on interval-integrable functions.

theorem TauCeti.fourierCoeffOn_sub {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hab : a < b) {f g : ℝ → E} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hg : IntervalIntegrable g MeasureTheory.volume a b) (n : ℤ) : fourierCoeffOn hab (fun (t : ℝ) => f t - g t) n = fourierCoeffOn hab f n - fourierCoeffOn hab g n

Fourier coefficients on an interval are subtractive on interval-integrable functions.

theorem TauCeti.norm_fourierCoeffOn_le {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hab : a < b) {g : ℝ → E} {M : ℝ} (hM : ∀ x ∈ Set.Ioc a b, ‖g x‖ ≤ M) (n : ℤ) : ‖fourierCoeffOn hab g n‖ ≤ M

A pointwise bound on a function over the interval (a, b] bounds its Fourier coefficients on [a, b].

theorem TauCeti.fourierCoeffOn_fourier {a b : ℝ} (hab : a < b) (m n : ℤ) : fourierCoeffOn hab (fun (t : ℝ) => (fourier m) ↑t) n = Pi.single m 1 n

On [a, b], the m-th Fourier monomial of period b - a has Fourier coefficient one at frequency m and zero at every other frequency.

theorem TauCeti.fourierCoeffOn_const_add_mul_fourier {a b : ℝ} (hab : a < b) (c w : ℂ) (m n : ℤ) : fourierCoeffOn hab (fun (t : ℝ) => c + w * (fourier m) ↑t) n = Pi.single 0 c n + Pi.single m w n

The Fourier coefficients on [a, b] of the circle c + w e^{2πimt/(b-a)} are c at frequency 0 and w at frequency m, added together when m = 0.

theorem TauCeti.eqOn_Icc_of_fourierCoeffOn_eq {a b : ℝ} (hab : a < b) {f g : ℝ → ℂ} (hf : ContinuousOn f (Set.uIcc a b)) (hg : ContinuousOn g (Set.uIcc a b)) (h : ∀ (n : ℤ), fourierCoeffOn hab f n = fourierCoeffOn hab g n) : Set.EqOn f g (Set.Icc a b)

Uniqueness of Fourier coefficients on an interval. Two complex functions continuous on [a, b] with the same Fourier coefficients on [a, b] agree on [a, b].

theorem TauCeti.exists_eqOn_const_add_mul_fourier_iff {a b : ℝ} (hab : a < b) {f : ℝ → ℂ} (hf : ContinuousOn f (Set.uIcc a b)) {s : ℤ} : (∃ (c : ℂ) (w : ℂ), ∀ t ∈ Set.Icc a b, f t = c + w * (fourier s) ↑t) ↔ ∀ (n : ℤ), n ≠ 0 → n ≠ s → fourierCoeffOn hab f n = 0

A complex function continuous on [a, b] agrees there with the circle c + w e^{2πist/(b-a)} for some c and w exactly when its Fourier coefficients on [a, b] vanish outside the frequencies 0 and s; c and w are then its coefficients at 0 and s when s ≠ 0.

theorem TauCeti.fourierCoeff_eq_fourierCoeffOn {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) (f : AddCircle T → ℂ) (n : ℤ) : fourierCoeff f n = fourierCoeffOn ⋯ (fun (x : ℝ) => f ↑x) n

The Fourier coefficients of a function on AddCircle T are those of its lift to ℝ on any period interval (a, a + T].

theorem TauCeti.exists_Lp_fourierCoeff_eq_fourierCoeffOn {a b : ℝ} [Fact (0 < b - a)] (hab : a < b) {g : ℝ → ℂ} (hgL2 : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) : ∃ (G : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)), ∀ (n : ℤ), fourierCoeff (↑↑G) n = fourierCoeffOn hab g n

A square-integrable function on (a, b] is the restriction of an L² class on the circle of length b - a with the same Fourier coefficients.

theorem TauCeti.fourierCoeffOn_iteratedDeriv {T : ℝ} [hT : Fact (0 < T)] {f : ℝ → ℂ} {k : ℕ} (hf : ContDiff ℝ (↑k) f) (hper : Function.Periodic f T) (a : ℝ) (n : ℤ) {j : ℕ} (hj : j ≤ k) : fourierCoeffOn ⋯ (iteratedDeriv j f) n = (2 * ↑Real.pi * Complex.I * ↑n / ↑T) ^ j * fourierCoeffOn ⋯ f n

Each derivative of a C^k function of period T multiplies its Fourier coefficients on a period interval by 2πin / T. At frequency 0 this says that the derivatives have mean zero.

theorem TauCeti.fourierCoeff_of_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {T : ℝ} [hT : Fact (0 < T)] [CompleteSpace E] {f g : AddCircle T → E} (hf : ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) => f ↑y) (g ↑x) x) (hg : Continuous g) (n : ℤ) : fourierCoeff g n = (2 * ↑Real.pi * Complex.I * ↑n / ↑T) • fourierCoeff f n

Differentiating a function on AddCircle T multiplies its Fourier coefficients by 2πin / T, for functions with values in any complete normed complex space: if the lift of f to ℝ has the continuous derivative g, then ĝ(n) = 2πin / T • f̂(n).