Kinetic energy of Schwartz states

The Fourier kinetic form agrees with the integral of squared coordinate derivatives on Schwartz states.

theorem LiebThirring.kineticEnergy_schwartz (N q : ℕ) (f : SchwartzMap (Configuration N) (SpinAmplitudes N q)) : kineticEnergy (f.toLp 2 MeasureTheory.volume) = ∑ i : Fin N, ∑ a : Fin 3, ∫⁻ (x : Configuration N), ↑‖(fderiv ℝ (fun (y : Configuration N) => f y) x) (PiLp.single 2 (i, a) 1)‖₊ ^ 2