Periodic one-dimensional Fourier integration by parts

This module isolates the boundary cancellation used by the eighth-order relative-translation argument. It works on the paper interval [-π, π], whose length is the torus period 2π.

theorem Anderson4D.fourierCoeffOn_negPi_pi_eq_inv_I_mul_deriv {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hf : ∀ x ∈ Set.uIcc (-Real.pi) Real.pi, HasDerivAt f (f' x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume (-Real.pi) Real.pi) (hperiod : f Real.pi = f (-Real.pi)) : fourierCoeffOn ⋯ f n = (Complex.I * ↑n)⁻¹ * fourierCoeffOn ⋯ f' n

One integration by parts on [-π, π] for a periodic function.

Because the interval length is exactly 2π, the normalized Fourier coefficient gains the scalar (I n)⁻¹ with no additional normalization factor.

theorem Anderson4D.norm_fourierCoeffOn_negPi_pi_le_inv_abs_mul_deriv {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hf : ∀ x ∈ Set.uIcc (-Real.pi) Real.pi, HasDerivAt f (f' x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume (-Real.pi) Real.pi) (hperiod : f Real.pi = f (-Real.pi)) : ‖fourierCoeffOn ⋯ f n‖ ≤ |↑n|⁻¹ * ‖fourierCoeffOn ⋯ f' n‖

Norm form of one periodic integration by parts.