Exact energy balance for divergence-free mild data

The Fourier energy identity loses no initial energy when the datum already lies in the range of the Leray projection.

theorem CKN.Leray.forcedMild_energy_balance_eq (b : ↥RealVectorL2) (hb : RegularizedMildJData b) {F : ℝ → ↥RealTensorL2} (hF : MeasureTheory.StronglyMeasurable F) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) {T C : ℝ} (hC : 0 ≤ C) (hFC : ∀ s ∈ Set.Ioc 0 T, ‖F s‖ ≤ C) (hH2 : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume) {t : ℝ} (ht : 0 ≤ t) (htT : t ≤ T) : (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 t), MeasureTheory.Integrable (fun (ξ : Foundation.Parabolic.L2Vec3) => forcedFourierLam ξ * ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (forcedComplexCurve b F h s)) ξ‖ ^ 2) MeasureTheory.volume) ∧ MeasureTheory.IntegrableOn (fun (s : ℝ) => forcedFourierDissipation (forcedComplexCurve b F h s)) (Set.Ioc 0 t) MeasureTheory.volume ∧ ‖forcedComplexCurve b F h t‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 t, forcedFourierDissipation (forcedComplexCurve b F h s) = (‖b‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 t, forcedStokesPairing (forcedComplexCurve b F h s) (complexifyTensorL2 (F s))) + 2 * ∫ (s : ℝ) in Set.Ioc 0 t, inner ℝ (forcedMildCurve b h F s) (h s)

The forced mild equation has an exact energy balance when its initial field lies in the divergence-free subspace.