Schwartz Fourier identities for kinetic energy

Extended Plancherel and the squared directional derivative formula for Schwartz functions use Mathlib’s exp(-2πi⟪ξ,x⟫) convention.

theorem LiebThirring.Fourier.lintegral_norm_sq_eq_ofReal_integral {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (f : SchwartzMap V H) : ∫⁻ (x : V), ↑‖f x‖₊ ^ 2 = ENNReal.ofReal (∫ (x : V), ‖f x‖ ^ 2)

Identify the nonnegative squared-norm integral with its real integral.

theorem LiebThirring.Fourier.lintegral_norm_sq_fourier {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H) : ∫⁻ (x : V), ↑‖(FourierTransform.fourier f) x‖₊ ^ 2 = ∫⁻ (x : V), ↑‖f x‖₊ ^ 2

Plancherel in nonnegative extended-integral form.

theorem LiebThirring.Fourier.norm_sq_fourier_lineDeriv {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (f : SchwartzMap V H) (m x : V) : ‖(FourierTransform.fourier (LineDeriv.lineDerivOp m f)) x‖ ^ 2 = (2 * Real.pi) ^ 2 * inner ℝ x m ^ 2 * ‖(FourierTransform.fourier f) x‖ ^ 2

The squared Fourier norm of a directional derivative, with the 2π factor.

theorem LiebThirring.Fourier.lintegral_fderiv_eq_fourier {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H) (m : V) : ∫⁻ (x : V), ↑‖(fderiv ℝ (fun (y : V) => f y) x) m‖₊ ^ 2 = ∫⁻ (x : V), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ENNReal.ofReal (inner ℝ x m ^ 2) * ↑‖(FourierTransform.fourier f) x‖₊ ^ 2

The directional derivative energy equals its weighted Fourier integral.