Iterated periodic Fourier integration by parts

This file iterates the one-step boundary-free identity on [-π, π]. The hypothesis records exactly the endpoint jets used in the iteration: orders strictly below the number of integrations by parts.

def Anderson4D.NegPiPiPeriodicJets (f : ℝ → ℂ) (r : ℕ) : Prop

Endpoint periodicity of the jets used in r integrations by parts.

Equations

• Anderson4D.NegPiPiPeriodicJets f r = ∀ j < r, iteratedDeriv j f Real.pi = iteratedDeriv j f (-Real.pi)

theorem Anderson4D.fourierCoeffOn_negPi_pi_eq_inv_I_pow_mul_iteratedDeriv {f : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (r : ℕ) (hf : ContDiff ℝ (↑r) f) (hperiod : NegPiPiPeriodicJets f r) : fourierCoeffOn ⋯ f n = (Complex.I * ↑n)⁻¹ ^ r * fourierCoeffOn ⋯ (iteratedDeriv r f) n

Exact r-fold periodic integration by parts on [-π, π].

theorem Anderson4D.norm_fourierCoeffOn_negPi_pi_le_inv_abs_pow_mul_iteratedDeriv {f : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (r : ℕ) (hf : ContDiff ℝ (↑r) f) (hperiod : NegPiPiPeriodicJets f r) : ‖fourierCoeffOn ⋯ f n‖ ≤ |↑n|⁻¹ ^ r * ‖fourierCoeffOn ⋯ (iteratedDeriv r f) n‖

Norm consequence of exact r-fold integration by parts.

theorem Anderson4D.norm_fourierCoeffOn_negPi_pi_le_average_norm (g : ℝ → ℂ) (n : ℤ) : ‖fourierCoeffOn ⋯ g n‖ ≤ (2 * Real.pi)⁻¹ * ∫ (t : ℝ) in -Real.pi..Real.pi, ‖g t‖

A normalized Fourier coefficient on [-π, π] is bounded by the normalized L¹ norm on that interval.

theorem Anderson4D.norm_fourierCoeffOn_negPi_pi_le_iteratedDeriv_integral {f : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (r : ℕ) (hf : ContDiff ℝ (↑r) f) (hperiod : NegPiPiPeriodicJets f r) : ‖fourierCoeffOn ⋯ f n‖ ≤ |↑n|⁻¹ ^ r * (2 * Real.pi)⁻¹ * ∫ (t : ℝ) in -Real.pi..Real.pi, ‖iteratedDeriv r f t‖

The final L¹ estimate after r periodic integrations by parts.

theorem Anderson4D.norm_fourierCoeffOn_negPi_pi_le_eighthDeriv_integral {f : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hf : ContDiff ℝ 8 f) (hperiod : NegPiPiPeriodicJets f 8) : ‖fourierCoeffOn ⋯ f n‖ ≤ |↑n|⁻¹ ^ 8 * (2 * Real.pi)⁻¹ * ∫ (t : ℝ) in -Real.pi..Real.pi, ‖iteratedDeriv 8 f t‖

Eight-fold periodic integration by parts in the form consumed by the relative-translation argument.