High-field mass and extended Fourier layer cake

Plancherel gives the literal strict high-frequency mass at each cutoff.

Integrating the strict threshold over real nonnegative energies gives its length.

theorem LiebThirring.lintegral_highFourierField {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) (hE : 0 ≤ E) : ∫⁻ (x : Position), ‖highFourierField h E x‖ₑ ^ 2 = ∫⁻ (ξ : Position), if E < fourierKineticMultiplier ξ then ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position H) h) ξ‖ₑ ^ 2 else 0

Plancherel gives the literal strict high-frequency mass at each cutoff.

theorem LiebThirring.lintegral_cutoff_threshold (threshold : ℝ) (a : ENNReal) : (∫⁻ (E : ℝ) in Set.Ici 0, if E < threshold then a else 0) = ENNReal.ofReal threshold * a

Integrating the strict threshold over real nonnegative energies gives its length.

theorem LiebThirring.lintegral_highFourierField_layerCake {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) : ∫⁻ (E : ℝ) in Set.Ici 0, ∫⁻ (x : Position), ‖highFourierField h E x‖ₑ ^ 2 = ∫⁻ (ξ : Position), ENNReal.ofReal (fourierKineticMultiplier ξ) * ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position H) h) ξ‖ₑ ^ 2

Tonelli integrates the high-field masses to the weighted outer Fourier energy.