Fourier coefficients of absolutely continuous functions

For an absolutely continuous function into a finite-dimensional complex normed space on a compact interval, integration by parts identifies the Fourier coefficients of its almost-everywhere derivative, including the endpoint contribution. For a closed curve the endpoint term vanishes; for a complex-valued closed curve f and real k, the coefficients of f' - i k f are therefore i (2πn / (b - a) - k) times those of f (TauCeti.fourierCoeffOn_sub_mul_I_mul). For complex-valued curves, Parseval gives an exact expression for the derivative energy as a frequency-weighted sum of squared coefficients. These identities allow sharp periodic inequalities to be proved directly at absolutely continuous regularity, without a passage through smooth approximation.

The Fourier convention and normalization are Mathlib's fourierCoeffOn: the frequency is 2πn / (b - a) and Parseval uses the interval average of the squared norm. The integration-by-parts calculation extends Mathlib's fourierCoeffOn_of_hasDeriv_right to almost-everywhere derivatives; the energy identity uses hasSum_sq_fourierCoeffOn.

theorem TauCeti.fourierCoeffOn_ae_derivative {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {f f' : ℝ → E} (hab : a < b) (hf : AbsolutelyContinuousOnInterval f a b) (hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (n : ℤ) : fourierCoeffOn hab f' n = (b - a)⁻¹ • (fourier (-n)) ↑a • (f b - f a) + (2 * ↑Real.pi * Complex.I * ↑n / (↑b - ↑a)) • fourierCoeffOn hab f n

The Fourier coefficient of an almost-everywhere derivative of an absolutely continuous function, with the endpoint term retained. The identity holds at every frequency, including zero, and does not require equal endpoint values.

theorem TauCeti.fourierCoeffOn_ae_derivative_of_eq_endpoints {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {f f' : ℝ → E} (hab : a < b) (hf : AbsolutelyContinuousOnInterval f a b) (hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (hfab : f a = f b) (n : ℤ) : fourierCoeffOn hab f' n = (2 * ↑Real.pi * Complex.I * ↑n / (↑b - ↑a)) • fourierCoeffOn hab f n

For an absolutely continuous closed curve, differentiation multiplies its n-th Fourier coefficient by 2πin / (b - a). In particular, the derivative has zero mean.

theorem TauCeti.fourierCoeffOn_sub_mul_I_mul {a b : ℝ} {f f' : ℝ → ℂ} (hab : a < b) (hf : AbsolutelyContinuousOnInterval f a b) (hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (hfab : f a = f b) (k : ℝ) (n : ℤ) : fourierCoeffOn hab (fun (t : ℝ) => f' t - ↑k * Complex.I * f t) n = ↑(2 * Real.pi * ↑n / (b - a) - k) * Complex.I * fourierCoeffOn hab f n

For an absolutely continuous closed complex curve and any real k, the Fourier coefficients of f' - i k f are i (2πn / (b - a) - k) times those of f, at the same frequency n: differentiation multiplies the n-th coefficient by 2πin / (b - a).

theorem TauCeti.hasSum_sq_frequency_mul_sq_fourierCoeffOn {a b : ℝ} {f f' : ℝ → ℂ} (hab : a < b) (hf : AbsolutelyContinuousOnInterval f a b) (hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (hfab : f a = f b) (hf' : MeasureTheory.MemLp f' 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) : HasSum (fun (n : ℤ) => (2 * Real.pi * ↑n / (b - a)) ^ 2 * ‖fourierCoeffOn hab f n‖ ^ 2) ((b - a)⁻¹ * ∫ (t : ℝ) in a..b, ‖f' t‖ ^ 2)

Parseval's energy identity for an absolutely continuous closed complex curve with square-integrable derivative. Each frequency contributes its squared frequency times the squared norm of the corresponding Fourier coefficient.