Periodicity supplies the endpoint jets for Fourier integration by parts

The iterated derivative of a translated function is the corresponding translate of its iterated derivative. Hence a literal 2π-periodicity identity supplies every endpoint-jet equality required by the repeated integration-by-parts theorem.

theorem Anderson4D.negPiPiPeriodicJets_of_two_pi_periodic {f : ℝ → ℂ} (hperiod : ∀ (t : ℝ), f (t + 2 * Real.pi) = f t) (r : ℕ) : NegPiPiPeriodicJets f r

A literal 2π-periodicity identity supplies all endpoint jets on [-π, π].

theorem Anderson4D.SmoothCutoff.negPiPiPeriodicJets_etaPeriodizationR4_coordLine (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (i : Fin dim) (r : ℕ) : NegPiPiPeriodicJets (fun (t : ℝ) => ↑(ρ.etaPeriodizationR4 ε (Function.update x i t))) r

The coordinate-line covariance periodization has all endpoint jets needed for eight periodic integrations by parts.